First-order tableau methods

MaRDI QIDQ2753598zbMATH OpenFDO

Authors Reinhold Letz

Publication date 14 November 2001

Mathematics Subject Classification ID

General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to mathematical logic and foundations (03-00) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Review text

See the review of the entire collection (Zbl 0956.03001).NEWLINENEWLINEFor the entire collection see [Zbl 0956.03001].

Cited in

(10)

• \textsf{Goéland}: a concurrent tableau-based theorem prover (system description)
• Craig interpolation with clausal first-order tableaux
• An efficient relational deductive system for propositional non-classical logics
• First-order dialogical games and tableaux
• scientific article; zbMATH DE number 834570 (Why is no real title available?)
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• Graded tableaux for Rational Pavelka Logic
• Range-restricted and Horn interpolation through clausal tableaux
• A tableau system for first-order logic with standard names
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux

This page was built for publication: First-order tableau methods

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2753598)