Catálogo de publicaciones - libros

The satisfiability checking problem is known to be decidable for a variety of modal/temporal logics such as the modal -calculus, but effective implementation has not necessarily been developed for all such logics. In this paper, we propose a decision procedure using the tableau method for the alternation-free two-way modal -calculus. Although the size of the tableau set maintained in the method might be large for complex formulas, the set and the operations on it can be expressed using BDD and therefore we can implement the method in an effective way.

Gödel’s Second Incompleteness Theorem states axiom systems of sufficient strength are unable to verify their own consistency. We will show this theorem does not preclude axiomizations for a computer’s floating point arithmetic from recognizing their own consistency, in certain well defined partial respects.

This paper presents the planning system Pdk (Planning with Domain Knowledge), based on the translation of planning problems into Linear Time Logic theories, in such a way that finding solution plans is reduced to model search. The model search mechanism is based on temporal tableaux. The planning language accepted by the system allows one to specify extra problem dependent information, that can be of help both in reducing the search space and finding plans of better quality.

For applications of first-order automated theorem provers in a wider verification context it is essential to provide a means of presenting and checking automatically found proofs. In this paper we present a new method of transforming disconnection tableau proofs found by the prover system DCTP into a series of resolution inferences representing a resolution refutation of the proof problem.

In this paper we describe a generic tableaux system for building models or counter-models and testing satisfiability of formulas in modal and description logics. This system is called LoTREC2.0. It is characterized by a high-level language for tableau rules and strategies. It aims at covering all Kripke-semantic based logics. It is implemented in Java and characterized by a user-friendly graphical interface. It can be used as a learning system for possible worlds semantics and tableaux based proof methods.

This paper describes the implementation of a tableau-based reasoning component which is capable of providing quasi natural language explanations for subsumptions within TBoxes.

In this paper we present CondLean 3.0, a theorem prover for propositional conditional logics CK, CK+ID, CK+MP, CK+CS, CK+CEM and some of their combinations. CondLean 3.0 implements sequent calculi for these logics. CondLean 3.0 improves CondLean and is developed following the methodology of leanTAP. It is implemented in SICStus Prolog and also comprises a graphical user interface implemented in JAVA. CondLean 3.0 can be downloaded at

The Intuitionistic Logic Theorem Proving (ILTP) Library provides a platfom for testing and benchmarking theorem provers for first-order intuitionistic logic. It includes a collection of benchmark problems in a standardised syntax and performance results obtained by a comprehensive test of currently available intuitionistic theorem proving systems. These results are used to provide information about the status and the difficulty rating of the benchmark problems.

Unit propagation is one of the most important techniques of efficient SAT solvers. Unfortunately, this technique is not directly applicable to first-order clausal tableaux. We show a way of integrating a variant of unit propagation into the disconnection calculus and present some results obtained with an implementation of unit propagation in the DCTP theorem prover that show the usefulness of our new method.