The liberalized \(\delta\)-rule in free variable semantic tableaux
From MaRDI portal
Publication:1344882
DOI10.1007/BF00881956zbMath0826.03005OpenAlexW1993434661MaRDI QIDQ1344882
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
Related Items
Free-variable semantic tableaux for the logic of fuzzy inequalities, On the complexity of proof deskolemization, A tableau prover for domain minimization, Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \), Infinite-Valued First-Order Łukasiewicz Logic: Hypersequent Calculi Without Structural Rules and Proof Search for Sentences in the Prenex Form, A deductive approach towards reasoning about algebraic transition systems, A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux, Incremental variable splitting, A framework for using knowledge in tableau proofs, Incremental theory reasoning methods for semantic tableaux, On the intuitionistic force of classical search (Extended abstract), The tableau-based theorem prover 3 T A P Version 4.0, On the intuitionistic force of classical search, Differential dynamic logic for hybrid systems, First order Stålmarck. Universal lemmas through branch merges, Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
Cites Work
