Journal of Automated Reasoning
Công bố khoa học tiêu biểu
* Dữ liệu chỉ mang tính chất tham khảo
Sắp xếp:
The addition of bounded quantification and partial functions to a computational logic and its theorem prover
Journal of Automated Reasoning - Tập 4 - Trang 117-172 - 1988
We describe an extension to our quantifier-free computational logic to provide the expressive power and convenience of bounded quantifiers and partial functions. By quantifier we mean a formal construct which introduces a bound or indicial variable whose scope is some subexpression of the quantifier expression. A familiar quantifier is the Σ operator which sums the values of an expression over som......
A Full Formalization of SLD-Resolution in the Calculus of Inductive Constructions
Journal of Automated Reasoning - Tập 23 - Trang 347-371 - 1999
This paper presents a full formalization of the semantics of definite programs, in the calculus of inductive constructions. First, we describe a formalization of the proof of first-order terms unification: this proof is obtained from a similar proof dealing with quasi-terms, thus showing how to relate an inductive set with a subset defined by a predicate. Then, SLD-resolution is explicitely define......
Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof
Journal of Automated Reasoning - Tập 64 - Trang 555-578 - 2019
In this article, we investigate the automated verification of temporal properties of heap-aware programs. We propose a deductive reasoning approach based on cyclic proof. Judgements in our proof system assert that a program has a certain temporal property over memory state assertions, written in separation logic with user-defined inductive predicates, while the proof rules of the system unfold tem......
Locales: A Module System for Mathematical Theories
Journal of Automated Reasoning - Tập 52 - Trang 123-153 - 2013
Locales are a module system for managing theory hierarchies in a theorem prover through theory interpretation. They are available for the theorem prover Isabelle. In this paper, their semantics is defined in terms of local theories and morphisms. Locales aim at providing flexible means of extension and reuse. Theory modules (which are called locales) may be extended by definitions and theorems. In......
Things to Know when Implementing KBO
Journal of Automated Reasoning - - 2006
The Knuth–Bendix ordering (KBO) is one of the term orderings in widespread use. We present a new algorithm to compute KBO, which is (to our knowledge) the first asymptotically optimal one. Starting with an ‘obviously correct’ version, we use program transformation to stepwise develop an efficient version, making clear the essential ideas, while retaining correctness. By theoretical analysis we sho......
Combining Sets with Cardinals
Journal of Automated Reasoning - Tập 34 - Trang 1-29 - 2005
We introduce a quantifier-free set-theoretic language for combining sets with elements in the presence of the cardinality operator. We prove that the language is decidable by providing a combination method specifically tailored to the combination domain of sets, cardinal numbers, and elements. Our method uses as black boxes a decision procedure for the elements and a decision procedure for cardina......
New uses of linear arithmetic in automated theorem proving by induction
Journal of Automated Reasoning - Tập 16 - Trang 39-78 - 1996
Zhang, Kapur, and Krishnamoorthy introduced a cover set method for designing induction schemes for automating proofs by induction from specifications expressed as equations and conditional equations. This method has been implemented in the theorem prover Rewrite Rule Laboratory (RRL) and a proof management system Tecton built on top of RRL, and it has been used to prove many nontrivial theorems an......
Intractable unifiability problems and backtracking
Journal of Automated Reasoning - Tập 5 - Trang 37-47 - 1989
Restrictions of the problem of finding all maximal unifiable or minimal nonunifiable subsets to those of certain sizes are shown to be NP-hard, and consequently inappropriate in general for reducing thrashing by intelligent backtracking in resolution theorem provers and logic program executions. We also show that existing backtrack methods based on the computation of all maximal unifiable subsets ......
Interweaving knowledge extracting, organizing and evaluating: A concrete design for preventing logic and structure bugs while interviewing experts
Journal of Automated Reasoning - Tập 6 - Trang 299-317 - 1990
The process of constructing expert systems (ESs), programs that approximate how domain experts solve problems in their specialized fields, is not at all as systematic, efficient, and verifiable as it should be. A reason is that no rigorous error-prevention interviewing method exists for structuring and testing ESs while building them. Often domain experts do implicitly ask of themselves analytical......
Tổng số: 936
- 1
- 2
- 3
- 4
- 5
- 6
- 10