The liberalized -rule in free variable semantic tableaux

DOI10.1007/BF00881956zbMATH Open0826.03005OpenAlexW1993434661MaRDI QIDQ1344882FDOQ1344882

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

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

zbMATH Keywords

semantic tableauxsoundnesscorrectness\(\delta+\)-rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Negation in logic programming
• Title not available (Why is that?)
• Situations, language and logic
• First-order modal tableaux

Cited In (22)

• A deductive approach towards reasoning about algebraic transition systems
• Free-variable semantic tableaux for the logic of fuzzy inequalities
• Reasoning with preorders and dynamic sorts using free variable tableaux
• Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
• A framework for using knowledge in tableau proofs
• On the intuitionistic force of classical search
• Title not available (Why is that?)
• First order Stålmarck. Universal lemmas through branch merges
• Title not available (Why is that?)
• Title not available (Why is that?)
• Differential dynamic logic for hybrid systems
• \(\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} \)
• Title not available (Why is that?)
• 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
• On the intuitionistic force of classical search (extended abstract)

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)