Tractability through symmetries in propositional calculus

DOI10.1007/BF00881844zbMath0804.68134OpenAlexW2037593836MaRDI QIDQ1332641

Belaïd Benhamou, Lakhdar Saïs

Publication date: 31 August 1994

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00881844

zbMATH Keywords

theorem provingsymmetriespropositional calculusunsatisfiabilityRamsey's problem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ramsey theory (05D10)

Related Items (9)

Predicting and detecting symmetries in FOL finite model search ⋮ Local and global symmetry breaking in itemset mining ⋮ SYMMETRIES IN MODAL LOGICS ⋮ Symmetric blocking ⋮ Homomorphisms of conjunctive normal forms. ⋮ Local Symmetry Breaking During Search in CSPs ⋮ Tractability of cut-free Gentzen type propositional calculus with permutation inference ⋮ Ground resolution with group computations on semantic symmetries ⋮ An adaptive prefix-assignment technique for symmetry reduction

Cites Work

• Unnamed Item
• Short proofs for tricky formulas
• Short proofs of the pigeonhole formulas based on the connection method
• Linear resolution with selection function
• On the maximal triangle-free edge-chromatic graphs in three colors
• A Computing Procedure for Quantification Theory

This page was built for publication: Tractability through symmetries in propositional calculus