Decision Making as Theorem Proving

We present a method for using type theory to solve decision making problem. Our method is based on the view that decision making is a special kind of theorem proving activity. An isomorphism between problems and types, and solutions and programs has been established to support this view which is much similar to the Curry-Howard isomorphism between propositions and types, and proofs and programs. To support our method, a proof development system called PowerEpsilon has been developed, and the synthesis of a decision procedure for validity of first-order propositional logic is discussed to show the power of the system.

Convergence Proving of the Theoretical&True Elongation Inequalities by Derivation and Analogy

According to LN?,theoretical&true elongation of tensile,and by adopting the increasing function of formulas with the derivation and analogy methods,the elongation formula of 0<(1+ε)^1/ε<e&0<ε^1/ε<1&four convergences are deduced too whenε>1 and 0<ε<1.The inequalities of LNε<εand LN(1+ε)<εand LN(1+ε)>LNεare deduced ifε>1 and 0<ε<1 in material dynamics.Finally the conclusions of LNε<εand LNε<LN(1+ε)<εare deduced together ifε>1 and 0<ε<1.

Proving Inequalities

Proving inequalities means to establish that theinequality holds true for arbitrary admissible valuesof the parameters.Example 1:Prove that the absolute value of asum does not exceed the sum of the absolute values:|a+b|≤|a|+|b|.①Proof.The absolute value of the sum |a+b| isequal to a+b or to -(a+b).From the definition ofthe absolute value we havea≤|a|,b≤|b|and combining these inequalities termwise,we geta+b≤|a|+|b|.②In exactly the same manner,-a≤|a|,-b<|b| and-(a+b)≤|a|+|b|.③From the inequalities ②,③ and the definition of

Refinement modeling and verification of secure operating systems for communication in digital twins

In traditional digital twin communication system testing,we can apply test cases as completely as possible in order to ensure the correctness of the system implementation,and even then,there is no guarantee that the digital twin communication system implementation is completely correct.Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly.In this paper,we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture,and to model the related assembly instructions.The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states,indicating that the system meets the design expectations.

Fast Theorem-Proving and Wu's Method

In this paper, the possibility of fast algorithm is discussed for me-chanical theorem proving, where the degeneracy condition are considered in designingof these algorithms. It is found that all of the methods depend seriously on some prin-ciples appearing in Wu's Method. In other words, some principles in Wu's Methodare the instinctive properties in these new fast algorithms of theorem proving.

Automated Theorem Proving Practice with Null Geometric Algebra

This paper presents the practice of automated theorem proving in Euclidean geometry with null geometric algebra, a combination of Conformal Geometric Algebra and Grassmann-Cayley algebra. This algebra helps generating extremely short and readable proofs: The proofs generated are mostly one-termed or two-termed. Besides, the theorems are naturally extended from qualitative description to quantitative characterization by removing one or more geometric constraints from the hypotheses.

Mechanical Geometry Theorem Proving Based on Groebner Bases

A new method for the mechanical elementary geometry theorem proving is presented by using Groebner bases of polynomial ideals. It has two main advantages over the approach proposed in literature: (i) It is complete and not a refutational procedure; (ii) The subcases of the geometry statements which are not generally true can be differentiated clearly.

Affine bracket algebra theory and algorithms and their applications in mechanical theorem proving

This paper discusses two problems:one is some important theories and algorithms of affine bracket algebra;the other is about their applications in mechanical theorem proving.First we give some efficient algorithms including the boundary expanding algorithm which is a key feature in application.We analyze the characteristics of the boundary operator and this is the base for the implementation of the system.We also give some new theories or methods about the exact division,the representations and structure of affine geometry and so on.In practice,we implement the mechanical auto-proving system in Maple 10 based on the above algorithms and theories.Also we test about more than 100 examples and compare the results with the methods before.

Geometry Theorem Proving by Decomposing Polynomial System into Strong Regular Sets

This paper presents a complete method to prove geometric theorem by decomposing the corresponding polynomial system. into strong regular sets, by which one can compute some components for which the geometry theorem is true and exclude other components for which the geometry theorem is false. Two examples are given to show that the geometry theorems are conditionally true for some components which are excluded by other methods.

Mechanical theorem proving in the surfaces using the characteristic set method and Wronskian determinant

In this paper, we generalize the method of mechanical theorem proving in curves to prove theorems about surfaces in differential geometry with a mechanical procedure. We improve the classical result on Wronskian determinant, which can be used to decide whether the elements in a partial differential field are linearly dependent over its constant field. Based on Wronskian determinant, we can describe the geometry statements in the surfaces by an algebraic language and then prove them by the characteristic set method.

PROVING-BY-EXAMPLES METHOD AND INCLUSION OF VARIETIES

Based on Ritt-Wu well ordering principle and Wu’s constructive theory of decomposing a polynomial set into irreducible ascending sets, we show that Hong’s 'Provingby Examples' method suits all theorems of equation type. Moreover, the de-

On first-order theorem proving using generalized odd-superpositions Ⅱ

It is shown that the proof system using odd-superpositions Ⅱ is not complete.The reason leading to this incompleteness is that the use of idempotency rule is neglected.By defining the superpositions of first-order polynomials and zero,the concept of odd-superpositions Ⅱ is extended,and a complete proof system using the extended odd-superpositions Ⅱ is developed.In addition,this proof system is an improvement on remainder method;its completeness demonstrates actually that the remainder method using semantic strategy is still complete.

Automated Theorem Proving in Temporal Logic:T-Resolution

This paper presentes a novel resolution method, T-resolution, based on the first order temporal logic. The primary claim of this method is its soundness and completeness. For this purpose, we construct the corresponding semantic trees and extend Herbrand's Theorem.

Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving

Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational problem.Traditionally,such analyses are performed using paper-and-pencil proofs and the results are sometimes validated using simulation techniques.These techniques are informal and thus may result in an inaccurate analysis.In this paper,we propose a formal technique for analyzing the expected time complexity of algorithms using higher-order-logic theorem proving.The approach calls for mathematically modeling the algorithm along with its inputs,using indicator random variables,in higher-order logic.This model is then used to formally reason about the expected time complexity of the underlying algorithm in a theorem prover.The paper includes the higher-order-logic formalization of indicator random variables,which are fundamental to the proposed infrastructure.In order to illustrate the practical effiectiveness and utilization of the proposed infrastructure,the paper also includes the analysis of algorithms for three well-known problems,i.e.,the hat-check problem,the birthday paradox and the hiring problem.

Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving

This paper introduces some improvements on the intelligent backtrackingstrategy for forward chaining theorem proving. How to decide a minimal useful consequent atom setfor a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessarynon-Horn clause used for forward chaining will be split only once. The increase of the search spaceby invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. Inthis paper, the principle of the proposed method and its correctness are introduced. Moreover, someexamples are provided to show that the proposed approach is powerful for forward chaining theoremproving.

An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving

This paper presents an improvement of Herbrand's theorem.We propose a method for specifying a subuniverse of the Herbrand universe of a clause set S for each argument of predicate symbols and function symbols in S.We prove that a clause set S is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of S that are derived by only instantiating each variable,which appears as an argument of predicate symbols or function symbols,in S over its corresponding argument's sub-universe of the Herbrand universe of S.Because such sub-universes are usually smaller(sometimes considerably)than the Herbrand universe of S,the number of ground instances may decrease considerably in many cases.We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set,and show the correctness of our improvement.Moreover,we introduce an application of our approach to model generation theorem proving for non-range-restricted problems,show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.

Combination of Model Checking and Theorem Proving to Verify Embedded Software

In this paper, a scheme of combining model checking and theorem proving techniques to verify high trustworthy embedded software is proposed. The software model described in state machine of unified model language is transformed into the input modeling language of a model checker in which the model is analyzed with associated property specifications expressed in temporal logic. The software model which has been verified by model checker is then transformed into abstract specifications of a theorem prover , in which the model will be refined, verified and translated into source C code. The transformation rules from state machine to input language of model checker and abstract specifications of theorem prover are given. The experiment shows that the proposed scheme can effectively improve the development and verification of high trustworthy embedded software.

Monetary Policy Proving Effective

Hu Xiaolian,Vice Governor of the People’s Bank of China,the country’s central bank, published an article concerning China’s managed floating exchange rate regime and the effectiveness of the monetary policy on the bank’s website on July 26.She pointed out monetary policy,as an important instrument of China’s macroeconomic control,has faced many challenges in recent years.A more flexible exchange rate regime will help improve the effectiveness of the policy.Edited excerpts follow

Introduction to the Proving Grounds in China

Outdoor tests are playing a more and more significant role in R & D of automobiles, especially prompt tests done in the proving ground which can extremely shorten the period of development. That is the reason that four proving ground have been set up in China. They are Hainan Proving Ground, Dongfeng Proving Ground, Dingyuan Proving Ground and Tongxian Proving Ground.

汽车可靠性道路试验仿真研究

应用Virtual Proving Ground软件进行汽车试验场可靠性道路试验的仿真研究,对交通部公路交通试验场标准搓板路面进行了三维实体建模,按照可靠性试验规范,在标准搓板路上对某国产轿车进行了计算机仿真,并与实车试验典型测点加速度-时间历程数据进行对比,具有很好的相似性;并对车辆模型进行了初步的可靠性分析。研究结果为进一步进行汽车可靠性耐久性研究提供了一定依据。