期刊文献+
共找到6篇文章
< 1 >
每页显示 20 50 100
Automated Theorem Proving in Temporal Logic:T-Resolution
1
作者 招兆铿 戴军 陈文丹 《Journal of Computer Science & Technology》 SCIE EI CSCD 1994年第1期53-62,共10页
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. 展开更多
关键词 Temporal logic automated theorem proving T-resolution reasoning soundness COMPLETENESS
原文传递
Geometry Theorem Proving by Decomposing Polynomial System into Strong Regular Sets 被引量:1
2
作者 Yong-BinLi WuLiu] Xiao-LinXiang 《Journal of Computer Science & Technology》 SCIE EI CSCD 2004年第6期820-827,共8页
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. 展开更多
关键词 zero decomposition strong regular set automated geometry theorem proving subsidiary condition
原文传递
REPRESENTATION AND AUTOMATED TRANSFORMATION OF GEOMETRIC STATEMENTS
3
作者 CHEN Xiaoyu 《Journal of Systems Science & Complexity》 SCIE EI CSCD 2014年第2期382-412,共31页
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. 展开更多
关键词 automated diagram drawing equivalent transformation formalized geometric statements geometric automated theorem proving.
原文传递
A Shape Graph Logic and A Shape System 被引量:5
4
作者 李兆鹏 张昱 陈意云 《Journal of Computer Science & Technology》 SCIE EI CSCD 2013年第6期1063-1084,共22页
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. 展开更多
关键词 shape graph logic program verification shape analysis automated theorem proving loop invariant inference
原文传递
Solution to the Generalized Champagne Problem on simultaneous stabilization of linear systems 被引量:4
5
作者 GUAN Qiang WANG Long +3 位作者 XIA BiCan YANG Lu YU WenSheng ZENG ZhenBing 《Science in China(Series F)》 2007年第5期719-731,共13页
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. 展开更多
关键词 linear systems STABILIZATION simultaneous stabilization Champagne Problem Generalized Champagne Problem complex analysis inequality-type theorem automated theorem proving
原文传递
Renaming a Set of Non-Horn Clauses
6
作者 聂旭民 郭青 《Journal of Computer Science & Technology》 SCIE EI CSCD 2000年第5期409-415,共7页
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. 展开更多
关键词 logic for artificial intelligence (AI) automated theorem proving logic programming Horn and non-Horn sets predicate renaming NP-COMPLETENESS
原文传递
上一页 1 下一页 到第
使用帮助 返回顶部