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.展开更多
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.展开更多
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...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.展开更多
该文旨在扼要介绍自动化定理证明(ATP)的发展历史与现状。其中,阐述了 ATP 的理论基础、基本原理和研究方向,列举了部分定理证明系统的主要功能和特征,并介绍了在此领域一些主要人物的基本思想和方法。同时,也对四色问题与初等几何定理...该文旨在扼要介绍自动化定理证明(ATP)的发展历史与现状。其中,阐述了 ATP 的理论基础、基本原理和研究方向,列举了部分定理证明系统的主要功能和特征,并介绍了在此领域一些主要人物的基本思想和方法。同时,也对四色问题与初等几何定理证明作了简单的讨论。最后,简单介绍了作者在 IBM—PC 机上实现的“格上的定理证明系统—TPSL”,并给出有关程序与算例。展开更多
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.展开更多
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.展开更多
The resolution method, proposed by J. A. Robinson in 1965, brought to many AI scholars’ attention. They made a lot of refinement or improvement on it, of which the famous ones are the semantic resolution brought in b...The resolution method, proposed by J. A. Robinson in 1965, brought to many AI scholars’ attention. They made a lot of refinement or improvement on it, of which the famous ones are the semantic resolution brought in by J. R. Slagle in 1967, the展开更多
基金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.
基金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 under Grant No.11671388CAS Project QYZDJ-SSW-SYS022GF S&T Innovation Special Zone Project
文摘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.
文摘该文旨在扼要介绍自动化定理证明(ATP)的发展历史与现状。其中,阐述了 ATP 的理论基础、基本原理和研究方向,列举了部分定理证明系统的主要功能和特征,并介绍了在此领域一些主要人物的基本思想和方法。同时,也对四色问题与初等几何定理证明作了简单的讨论。最后,简单介绍了作者在 IBM—PC 机上实现的“格上的定理证明系统—TPSL”,并给出有关程序与算例。
文摘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.
文摘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.
文摘The resolution method, proposed by J. A. Robinson in 1965, brought to many AI scholars’ attention. They made a lot of refinement or improvement on it, of which the famous ones are the semantic resolution brought in by J. R. Slagle in 1967, the
