The liberalized -rule in free variable semantic tableaux

DOI10.1007/BF00881956MaRDI QIDQ1344882zbMATH OpenOpenAlexFDO

Authors Reiner Hähnle, Peter H. Schmitt

Publication date 22 February 1995

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf00881956

zbMATH Keywords

semantic tableauxsoundnesscorrectness\(\delta+\)-rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1507185
• scientific article; zbMATH DE number 517067
• scientific article; zbMATH DE number 1552525
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• Free-variable tableaux for propositional modal logics

Cites work

• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 487143 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• First-order modal tableaux
• Negation in logic programming
• Situations, language and logic

Cited in

(22)

• On the intuitionistic force of classical search (extended abstract)
• A deductive approach towards reasoning about algebraic transition systems
• Free-variable semantic tableaux for the logic of fuzzy inequalities
• Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
• Reasoning with preorders and dynamic sorts using free variable tableaux
• A framework for using knowledge in tableau proofs
• On the intuitionistic force of classical search
• scientific article; zbMATH DE number 1189105 (Why is no real title available?)
• First order Stålmarck. Universal lemmas through branch merges
• Differential dynamic logic for hybrid systems
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 1507185 (Why is no real title available?)
• \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
• Incremental variable splitting
• The tableau-based theorem prover 3 T A P Version 4.0
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
• Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
• scientific article; zbMATH DE number 1507197 (Why is no real title available?)
• On the complexity of proof deskolemization
• Incremental theory reasoning methods for semantic tableaux
• A tableau prover for domain minimization
• Infinite-valued first-order Łukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form

This page was built for publication: The liberalized \(\delta\)-rule in free variable semantic tableaux

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