Splitting through new proposition symbols

DOI10.1007/3-540-45653-8_12zbMATH Open1275.03083OpenAlexW1480041003MaRDI QIDQ2996161FDOQ2996161

Authors: Hans de Nivelle 

Publication date: 6 May 2011

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-45653-8_12

Recommendations

• The 481 ways to split a clause and deal with propositional variables
• scientific article; zbMATH DE number 3959369
• Incremental variable splitting
• Playing with AVATAR
• Combining superposition, sorts and splitting

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (7)

• A new methodology for developing deduction methods
• Deciding expressive description logics in the framework of resolution
• Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments
• The 481 ways to split a clause and deal with propositional variables
• Case splitting in an automatic theorem prover for real-valued special functions
• First-order resolution methods for modal logics
• Labelled splitting

Uses Software

• SPASS
• Saturate

This page was built for publication: Splitting through new proposition symbols

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