Reductions for non-clausal theorem proving

DOI10.1016/S0304-3975(00)00044-XzbMath0989.68128OpenAlexW2102501380MaRDI QIDQ5958754

Inma P. de Guzmán, G. Aguilera, Manuel Ojeda Aciego, A. Valverde

Publication date: 3 March 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00044-x

zbMATH Keywords

SAT problemnon-clausal theorem provingprime implicates/implicants

Mathematics Subject Classification ID

Related Items (5)

General form of \(\alpha\)-resolution principle for linguistic truth-valued lattice-valued logic ⋮ Filter-based resolution principle for lattice-valued propositional logic LP\((X)\) ⋮ A first polynomial non-clausal class in many-valued logic ⋮ Generalizations of lattices via non-deterministic operators ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A satisfiability tester for non-clausal propositional calculus
• On the relative merits of path dissolution and the method of analytic tableaux
• Proof theory and automated deduction
• Hard random 3-SAT problems and the Davis-Putnam procedure
• Dissolution
• The relative efficiency of propositional proof systems

This page was built for publication: Reductions for non-clausal theorem proving