The European Journal on Artificial Intelligence

Monodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeMP. However, the architecture of TeMP cannot guarantee the fairness of its derivations. In this paper we present an architecture for a resolution-based monodic first-order temporal logic prover that can ensure fair derivations and we describe the implementation of this fair architecture in the theorem prover TSPASS.

Sophisticated reductions are an important means to achieve progress in automated theorem proving. We consider the powerful reduction rule Contextual Rewriting in connection with the superposition calculus. If considered in its most general form the applicability of contextual rewriting is not decidable. We develop an instance of contextual rewriting where applicability becomes decidable while preserving a great deal of its simplification power. A sophisticated implementation of the rule in SPASS reveals its application potential. Our contextual rewriting instance called subterm contextual rewriting is feasible in the sense that it can be executed on the overall TPTP resulting in a gain of solved problems and new solutions to a number of problems that could not be solved by theorem provers so far.

In this paper, we present a resolution-based calculus R_CTL^>,S for Computation Tree Logic (CTL) as well as an implementation of that calculus in the theorem prover CTL-RP. The calculus R_CTL^>,S requires a transformation of an arbitrary CTL formula to an equi-satisfiable clausal normal form formulated in an extension of CTL with indexed path formulae. The calculus itself consists of a set of resolution rules which can be used for an EXPTIME decision procedure for the satisfiability problem of CTL. We give a formal semantics for the clausal normal form, provide proof sketches for the soundness and completeness of the resolution rules, discuss the complexity of the decision procedure based on R_CTL^>,S, and present an approach to implementing the calculus R_CTL^>,S using first-order techniques. Finally, we give a comparison between CTL-RP and a tableau theorem prover for CTL.

The Suggested Upper Merged Ontology (SUMO) has provided the TPTP problem library with problems that have large numbers of axioms, of which typically only a few are needed to prove any given conjecture. The LTB division of the CADE ATP System Competition tests the performance of ATP systems on these types of problems. The SUMO problems were used in the SMO category of the LTB division in 2008. This paper presents an analysis of the performance of the 2007 and 2008 CASC entrants on the SUMO problems, illustrating the improvements that can be achieved by various tuning techniques.

Since Zhang and Malik's work in 2003 [19], it is well-known that modern DPLL-based SAT solvers with learning can be instrumented to write a trace on disk from which, if the input is unsatisfiable, a resolution proof can be extracted (and checked), and hence also an unsatisfiable core: a (frequently small) unsatisfiable subset of the input clauses.

In this article we first give a new algorithmic approach for processing these (frequently huge) traces. It achieves the efficiency of a depth-first traversal, while preserving the property that memory usage remains upper bounded by that of the SAT solver that generated the trace.

The second part of this article is about in-memory algorithms for generating SAT proofs and cores, without writing traces to disk. We discuss advantages and disadvantages of this approach and investigate why the current SAT solvers with this feature still run out of memory on long SAT runs. We analyze several of these in-memory algorithms, based on carefully designed experiments with our implementation of each one of them, as well as with (our implementation of) a trace-based one. Then we describe a new in-memory algorithm which saves space by doing more bookkeeping to discard unnecessary information, and show that it can handle significantly more instances than the previously existing algorithms, at a negligible expense in time.

Connection calculi benefit from a goal-oriented proof search, but are in general not proof confluent. A substantial amount of backtracking is required, which significantly affects the time complexity of the proof search. This paper presents a simple strategy for effectively restricting backtracking in connection calculi. In combination with a few basic techniques it provides the basis for a refined connection calculus. The paper also describes how this calculus can be implemented directly by a few lines of Prolog code. This very compact program is the core of an enhanced version of the automated theorem prover leanCoP. The performance of leanCoP is compared with other lean theorem provers, connection provers, and state-of-the-art theorem provers. The results show that restricted backtracking is a successful technique when performing proof search in connection calculi.

SOLAR (SOL for Advanced Reasoning) is a first-order clausal consequence finding system based on the SOL (Skip Ordered Linear) tableau calculus. The ability to find non-trivial consequences of an axiom set is useful in many applications of Artificial Intelligence such as theorem proving, query answering and nonmonotonic reasoning. SOL is a connection tableau calculus which is complete for finding the non-subsumed consequences of a clausal theory. SOLAR is an efficient implementation of SOL that employs several methods to prune away redundant branches of the search space. This paper introduces some of the key pruning and control strategies implemented in SOLAR and demonstrates their effectiveness on a collection of benchmark problems.

This article presents a hybrid Abox tableau calculus for 𝒮ℋ𝒬 which extends the basic description logic 𝒜ℒ𝒞 with role hierarchies, transitive roles, and qualified number restrictions. The prominent feature of our hybrid calculus is that it reduces reasoning about qualified number restrictions to integer linear programming. The calculus decides 𝒮ℋ𝒬 Abox consistency w.r.t. a Tbox containing general axioms. The presented approach ensures a more informed calculus which adequately handles the interaction between numerical and logical restrictions in 𝒮ℋ𝒬 concept and individual descriptions. A prototype reasoner for deciding 𝒜ℒ𝒞ℋ𝒬 concept satisfiability has been implemented. An empirical evaluation of our hybrid reasoner and its integrated optimization techniques for a set of synthesized benchmarks featuring qualified number restrictions clearly demonstrates the effectiveness of our hybrid calculus.

The LogAnswer system is an application of automated reasoning to the field of open domain question answering. In order to find answers to natural language questions regarding arbitrary topics, the system integrates an automated theorem prover in a framework of natural language processing tools. The latter serve to construct an extensive knowledge base automatically from given textual sources, while the automated theorem prover makes it possible to derive answers by deductive reasoning. In the paper, we discuss the requirements to the prover that arise in this application, especially concerning efficiency and robustness. The proposed solution rests on incremental reasoning, relaxation of the query (if no proof of the full query is found), and other techniques. In order to improve the robustness of the approach to gaps of the background knowledge, the results of deductive processing are combined with shallow linguistic features by machine learning.

We survey all known results in the area of quasigroup and loop theory to have been obtained with the assistance of automated theorem provers. We provide both informal and formal descriptions of selected problems, and compare the performance of selected state-of-the art first order theorem provers on them. Our analysis yields some surprising results, e.g., the theorem prover most often used by loop theorists does not necessarily yield the best performance.

This paper presents an interactive proof method for the verification of temporal properties of concurrent systems based on symbolic execution. Symbolic execution is a well known and very intuitive strategy for the verification of sequential programs. We have carried over this approach to the interactive verification of arbitrary linear temporal logic properties of (infinite state) parallel programs. The resulting proof method is very intuitive to apply and can be automated to a large extent. It smoothly combines first-order reasoning with reasoning in temporal logic. The proof method has been implemented in the interactive verification environment KIV and has been used in several case studies.