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 correspondi...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.展开更多
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...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.展开更多
The emergence of a large quantity of digital resources in geometry, various geometric automated theorem proving systems, and kinds of dynamic geometry software systems has made geometric computation, reasoning, drawin...The emergence of a large quantity of digital resources in geometry, various geometric automated theorem proving systems, and kinds of dynamic geometry software systems has made geometric computation, reasoning, drawing, and knowledge management dynamic, automatic or interactive on computer. Integration of electronic contents and different systems is desired to enhance their accessibility and exploitability. This paper proposes an equivalent transformation framework for manipulating geometric statements available in the literature by using geometry software systems. Such a framework works based on a newly designed geometry description language(GDL), in which geometric statements can be represented naturally and easily. The author discusses and presents key procedures of automatically transforming GDL statements into target system-native representations for manipulation.The author also demonstrates the framework by illustrating equivalent transformation processes and interfaces for compiling the transformation results into executable formats that can be interpreted by the target geometry software systems for automated theorem proving and dynamic diagram drawing.展开更多
Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program poi...Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties (e.g., orderedness). Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect (reflected in shape declarations) in the analysis stage. As a benefit, programmers need not provide specifications (e.g., pre-/post-conditions, loop invariants) about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.展开更多
The well-known Generalized Champagne Problem on simultaneous stabilization of linear systems is solved by using complex analysis and Blonders technique. We give a complete answer to the open problem proposed by Patel ...The well-known Generalized Champagne Problem on simultaneous stabilization of linear systems is solved by using complex analysis and Blonders technique. We give a complete answer to the open problem proposed by Patel et al., which automatically includes the solution to the original Champagne Problem. Based on the recent development in automated inequality-type theorem proving, a new stabilizing controller design method is established. Our numerical examples significantly improve the relevant results in the literature.展开更多
Several extensions of the logic programming language Prolog to non Horn clauses use case analysis to handle non-Horn clauses. In this paper, analytical and empirical evidences are presented to show that, by making a ...Several extensions of the logic programming language Prolog to non Horn clauses use case analysis to handle non-Horn clauses. In this paper, analytical and empirical evidences are presented to show that, by making a set of clauses less 'non-Horn' using predicate renaming, the performance of these case-analysis based procedures can be improved significantly. In addition, the paper also investigated the problem of efficiently constructing a predicate renaming that reduces the degree of 'non-Hornness' of a clause set maximally. It is shown that this problem of finding a predicate renaming to achieve minimal 'non-Hornness' is NP-complete.展开更多
文摘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.
文摘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.
基金supported partially by the SKLSDE Open Fund(SKLSDE-2011KF-02)the Natural Science Foundation of China under Grant No.61003139the MOE-Intel Joint Research Fund(MOE-INTEL-11-03)
文摘The emergence of a large quantity of digital resources in geometry, various geometric automated theorem proving systems, and kinds of dynamic geometry software systems has made geometric computation, reasoning, drawing, and knowledge management dynamic, automatic or interactive on computer. Integration of electronic contents and different systems is desired to enhance their accessibility and exploitability. This paper proposes an equivalent transformation framework for manipulating geometric statements available in the literature by using geometry software systems. Such a framework works based on a newly designed geometry description language(GDL), in which geometric statements can be represented naturally and easily. The author discusses and presents key procedures of automatically transforming GDL statements into target system-native representations for manipulation.The author also demonstrates the framework by illustrating equivalent transformation processes and interfaces for compiling the transformation results into executable formats that can be interpreted by the target geometry software systems for automated theorem proving and dynamic diagram drawing.
基金supported by the National Natural Science Foundation of China under Grant Nos.61003043,61170018the National High Technology Research and Development 863 Program of China under Grant No.2012AA010901-2the Postdoctoral Science Foundation of China under Grant No.2012M521250
文摘Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties (e.g., orderedness). Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect (reflected in shape declarations) in the analysis stage. As a benefit, programmers need not provide specifications (e.g., pre-/post-conditions, loop invariants) about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.
基金Supported by the National Natural Science Foundation of China (Grant Nos. 60572056, 60528007, 60334020, 60204006, 10471044, and 10372002)the National Key Basic Research and Development Program (Grant Nos. 2005CB321902, 2004CB318003, 2002CB312200)+1 种基金the Overseas Outstanding Young Researcher Foundation of Chinese Academy of Sciencesthe Program of National Key Laboratory of Intelligent Technology and Systems of Tsinghua University
文摘The well-known Generalized Champagne Problem on simultaneous stabilization of linear systems is solved by using complex analysis and Blonders technique. We give a complete answer to the open problem proposed by Patel et al., which automatically includes the solution to the original Champagne Problem. Based on the recent development in automated inequality-type theorem proving, a new stabilizing controller design method is established. Our numerical examples significantly improve the relevant results in the literature.
文摘Several extensions of the logic programming language Prolog to non Horn clauses use case analysis to handle non-Horn clauses. In this paper, analytical and empirical evidences are presented to show that, by making a set of clauses less 'non-Horn' using predicate renaming, the performance of these case-analysis based procedures can be improved significantly. In addition, the paper also investigated the problem of efficiently constructing a predicate renaming that reduces the degree of 'non-Hornness' of a clause set maximally. It is shown that this problem of finding a predicate renaming to achieve minimal 'non-Hornness' is NP-complete.