Liberalized variable splitting

DOI10.1007/S10817-006-9055-9zbMATH Open1121.03019OpenAlexW1988574992MaRDI QIDQ877894FDOQ877894

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

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

zbMATH Keywords

first-order logictableau calculusconnection method

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• An improved proof procedure1
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• Title not available (Why is that?)
• Connections in nonclassical logics
• Tableaux and related methods
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• Title not available (Why is that?)
• Theorem Proving via General Matings
• Using meta-variables for natural deduction in \textit{Theorema}
• IeanCOP: lean connection-based theorem proving
• Title not available (Why is that?)
• Automated Reasoning with Analytic Tableaux and Related Methods
• Free-variable tableaux for propositional modal logics

Cited In (6)

• Title not available (Why is that?)
• From Schütte’s Formal Systems to Modern Automated Deduction
• nanoCoP: A Non-clausal Connection Prover
• Incremental variable splitting
• A Non-clausal Connection Calculus
• A Labelled System for IPL with Variable Splitting

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)