Liberalized variable splitting

DOI10.1007/S10817-006-9055-9MaRDI QIDQ877894zbMATH OpenOpenAlexFDO

Authors Roger Antonsen, Arild Waaler

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)

Recommendations

• Incremental variable splitting
• Logics in Artificial Intelligence
• The 481 ways to split a clause and deal with propositional variables
• A free variable sequent calculus with uniform variable splitting
• Automated Reasoning with Analytic Tableaux and Related Methods

Cites work

• scientific article; zbMATH DE number 3821127 (Why is no real title available?)
• scientific article; zbMATH DE number 3904558 (Why is no real title available?)
• scientific article; zbMATH DE number 49746 (Why is no real title available?)
• scientific article; zbMATH DE number 517067 (Why is no real title available?)
• scientific article; zbMATH DE number 1552523 (Why is no real title available?)
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• scientific article; zbMATH DE number 194631 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• A free variable sequent calculus with uniform variable splitting
• An improved proof procedure1
• Automated Reasoning with Analytic Tableaux and Related Methods
• Connections in nonclassical logics
• Free-variable tableaux for propositional modal logics
• IeanCOP: lean connection-based theorem proving
• Tableaux and related methods
• Theorem Proving via General Matings
• Universal variables in disconnection tableaux
• Using meta-variables for natural deduction in \textit{Theorema}

Cited in

(8)

• A free variable sequent calculus with uniform variable splitting
• A Non-clausal Connection Calculus
• Incremental variable splitting
• A Labelled System for IPL with Variable Splitting
• nanoCoP: a non-clausal connection prover
• scientific article; zbMATH DE number 1507185 (Why is no real title available?)
• From Schütte’s Formal Systems to Modern Automated Deduction
• Automated Reasoning with Analytic Tableaux and Related Methods

Describes a project that uses

Uses Software

• ModLeanTAP

This page was built for publication: Liberalized variable splitting

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