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......
Proof-Guided Test Selection from First-Order Specifications with Equality
Journal of Automated Reasoning - Tập 45 - Trang 437-473 - 2009
This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ideal exhaustive test set to start the selection from. We then propose an extension of the test selection method called axiom unfolding, originally defined for algebraic specifications, to quantifier-free first-order specifi......
I-SATCHMO: An Improvement of SATCHMO
Journal of Automated Reasoning - Tập 27 - Trang 313-322 - 2001
We introduce a method for reducing the redundant search space for SATCHMO's model generation approach by means of intelligent backtracking. During the reasoning, we mark an asserted consequent atom as “useful” whenever it has been used as an antecedent atom for forward chaining. We show that a splitting of the consequence of a non-Horn clause is unnecessary if one of its consequent atoms is found ......
Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
Journal of Automated Reasoning - Tập 64 - Trang 1361-1391 - 2020
Chain reduction enables reduced ordered binary decision diagrams (BDDs) and zero-suppressed binary decision diagrams (ZDDs) to each take advantage of the other’s ability to symbolically represent Boolean functions in compact form. For any Boolean function, its chain-reduced ZDD (CZDD) representation will be no larger than its ZDD representation, and at most twice the size of its BDD representation......
Fast Term Indexing with Coded Context Trees
Journal of Automated Reasoning - Tập 32 - Trang 103-120 - 2004
Indexing data structures have a crucial impact on the performance of automated theorem provers. Examples are discrimination trees, which are like tries where terms are seen as strings and common prefixes are shared, and substitution trees, where terms keep their tree structure and all common contexts can be shared. Here we describe a new indexing data structure, called context trees, where, by mea......
Tổng số: 936
- 1
- 2
- 3
- 4
- 5
- 6
- 10