Incremental variable splitting

DOI10.1016/J.JSC.2011.12.032MaRDI QIDQ429591zbMATH OpenOpenAlexFDO

Authors Christian Mahesh Hansen, Roger Antonsen, Martin Giese, Arild Waaler

Publication date 20 June 2012

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jsc.2011.12.032

zbMATH Keywords

theorem provingtableauxvariable splittingincremental closure

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Liberalized variable splitting
• A free variable sequent calculus with uniform variable splitting
• Automated Reasoning with Analytic Tableaux and Related Methods
• The 481 ways to split a clause and deal with propositional variables
• scientific article; zbMATH DE number 1765699

Cites work

• scientific article; zbMATH DE number 1688810 (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 1543301 (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 Labelled System for IPL with Variable Splitting
• A Non-clausal Connection Calculus
• Automated Reasoning with Analytic Tableaux and Related Methods
• Liberalized variable splitting
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The liberalized -rule in free variable semantic tableaux

Cited in

(5)

• Splitting through new proposition symbols
• Automated Reasoning with Analytic Tableaux and Related Methods
• Liberalized variable splitting
• scientific article; zbMATH DE number 1765699 (Why is no real title available?)
• A free variable sequent calculus with uniform variable splitting

Describes a project that uses

Uses Software

• TPTP

This page was built for publication: Incremental variable splitting

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