An empirical analysis of modal theorem provers

DOI10.1080/11663081.1999.10510981zbMath1033.03501OpenAlexW2084802994MaRDI QIDQ4443417

Ullrich Hustadt, Renate A. Schmidt

Publication date: 13 January 2004

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1080/11663081.1999.10510981

zbMATH Keywords

modal logicautomated theorem provingempirical performance analysis

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items

Simulation and Synthesis of Deduction Calculi, Invariant-free clausal temporal resolution, Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models, First-Order Resolution Methods for Modal Logics, Unsorted Functional Translations, A new methodology for developing deduction methods, EXPtime tableaux for ALC

Uses Software

• SPASS

Cites Work

• Attributive concept descriptions with complements
• Modal tableau calculi and interpolation
• Proof methods for modal and intuitionistic logics
• TABLEAUX: A general theorem prover for modal logics
• An optimality result for clause form translation
• Are tableaux an improvement on truth-tables? Cut-free proofs and bivalence
• Gentzen systems for modal logic
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• Functional translation and second-order frame properties of modal logics