Tableaux and Dual Tableaux: Transformation of Proofs

Studia Logica 85 (3):283-302 (2007)
  Copy   BIBTEX

Abstract

We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two systems are dual to each other. The duality is expressed in a formal way which enables us to define a transformation of proofs in one of the systems into the proofs of the other.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,098

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Analytics

Added to PP
2009-01-28

Downloads
60 (#275,302)

6 months
6 (#587,658)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Joanna Golinska-Pilarek
University of Warsaw

References found in this work

The mathematics of metamathematics.Helena Rasiowa - 1963 - Warszawa,: Państwowe Wydawn. Naukowe. Edited by Roman Sikorski.
Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.
The foundations of mathematics.Evert Willem Beth - 1959 - Amsterdam,: North-Holland Pub. Co..
Socratic Proofs for Quantifiers★.Andrzej Wiśniewski & Vasilyi Shangin - 2006 - Journal of Philosophical Logic 35 (2):147-178.
A proof system for contact relation algebras.Ivo Düntsch & Ewa Orłowska - 2000 - Journal of Philosophical Logic 29 (3):241-262.

View all 7 references / Add more references