Catálogo de publicaciones - libros

The inverse method, due to Maslov, is a forward theorem proving method for cut-free sequent calculi that relies on the subformula property. The Logic of Bunched Implications (), due to Pym and O’Hearn, is a logic which freely combines the familiar connectives of intuitionistic logic with multiplicative linear conjunction and its adjoint implication. We present the first formulation of an inverse method for propositional without units. We adapt the sequent calculus for into a forward calculus. The soundness and completeness of the calculus are proved, and a canonical form for bunches is given.

Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathematical proofs. The cut-elimination method CERES (cut-elimination by resolution) works by constructing a set of clauses from a proof with cuts. Any resolution refutation of this set can then serve as a skeleton of a proof with only atomic cuts.

In this paper we present a systematic experiment with the implementation of CERES on a proof of reasonable size and complexity. It turns out that the proof with cuts can be transformed into two different proofs of the theorem. In particular, the application of positive and negative hyperresolution yield different mathematical arguments. As an unexpected side-effect the derived clauses of the resolution refutation proved particularly interesting as they can be considered as meaningful universal lemmas.

Though the proof under investigation is intuitively simple, the experiment demonstrates that new (and relevant) mathematical information on proofs can be obtained by computational methods. It can be considered as a first step in the development of an experimental culture of in mathematics.

We provide uniform and invertible logical rules in a framework of relational hypersequents for the three fundamental t-norm based fuzzy logics i.e., Łukasiewicz logic, Gödel logic, and Product logic. Relational hypersequents generalize both hypersequents and sequents-of-relations. Such a framework can be interpreted via a particular class of dialogue games combined with bets, where the rules reflect possible moves in the game. The problem of determining the validity of atomic relational hypersequents is shown to be polynomial for each logic, allowing us to develop Co-NP calculi. We also present calculi with very simple initial relational hypersequents that vary only in the structural rules for the logics.

The coupling of description logic reasoning systems with other reasoning formalisms (possibly over the Web) is becoming an important research issue and calls for advanced methods and algorithms. Recently, several notions of have been introduced, combining rule-based semantics with description logics. Among them are (or for short) which combine nonmonotonic logic programs with description logics under a generalized version of the answer-set and the well-founded semantics, respectively, which are the predominant semantics for nonmonotonic logic programs. In this paper, we consider some technical issues regarding an efficient implementation for both semantics, which has been realized in a working prototype exploiting the two state-of-art tools DLV and RACER. A major issue in this respect is efficient interfacing between the two reasoning systems at hand, for which we devised special methods. Such methods may fruitfully be used for the implementation of systems of similar nature. Reported experimentation activities with our prototype show that the methods we have developed are effective and are a key for highly optimized nonmonotonic dl-program engines.

The Tag-Frame system of resource management [1] reunited two divergent threads of linear logic programming research by achieving the efficient proof search behaviour of abstract systems, such as [2], while using a low-level tag-based approach, as in [3], suitable for specifying an abstract machine. However, Tag-Frame relies on set operations which are linear in the size of the sets, and is not as efficient, in general, as it could be. We present a new tag-based derivation system which relies solely on low-level concepts to implement efficient resource management, where most linear time operations have been replaced by constant time ones. Though motivated and informed by the Tag-Frame system, we derive our system directly from, and prove its correctness with respect to the system of Cervesato et al. [2]. An abstract machine based on the new system has been implemented by Tamura and Banbara, and its performance compared to their previous machine.

In this paper a proof technique for reasoning about the multi-modal logic of beliefs and goals is defined based on resolution at different levels of a tree of clauses. We have considered belief and goal as normal modal logic operators. The technique is inspired by that in [6,7] and allows for a locality property to be satisfied. The main motivation for this work arises not as much from theorem-proving as from the notion of belief and goal revision under an assumption of consistency of the beliefs and goals of an agent. We also present proofs of soundness and completeness of the logic.