Liberalized variable splitting

DOI10.1007/s10817-006-9055-9zbMath1121.03019OpenAlexW1988574992MaRDI QIDQ877894

Arild Waaler, Roger Antonsen

Publication date: 4 May 2007

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

Full work available at URL: https://doi.org/10.1007/s10817-006-9055-9

zbMATH Keywords

first-order logictableau calculusconnection method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Incremental variable splitting ⋮ A Non-clausal Connection Calculus ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ From Schütte’s Formal Systems to Modern Automated Deduction

Uses Software

• ModLeanTAP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• IeanCOP: lean connection-based theorem proving
• An improved proof procedure1
• Theorem Proving via General Matings
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods
• Automated Reasoning with Analytic Tableaux and Related Methods
• Free-variable tableaux for propositional modal logics