Subsumption Algorithms for Three-Valued Geometric Resolution

DOI10.1007/978-3-319-40229-1_18zbMath1405.68317arXiv1703.02830OpenAlexW2491947963MaRDI QIDQ2817925

Hans de Nivelle

Publication date: 5 September 2016

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

Full work available at URL: https://arxiv.org/abs/1703.02830

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

Subsumption Algorithms for Three-Valued Geometric Resolution ⋮ Theorem proving as constraint solving with coherent logic

Uses Software

• MiniSat
• Geo 2007F

Cites Work

• Unnamed Item
• Classical logic with partial functions
• Boosting search with variable elimination in constraint optimization and constraint satisfaction problems
• The CADE-16 ATP system competition
• Subsumption Algorithms for Three-Valued Geometric Resolution
• Theorem proving for classical logic with partial functions by reduction to Kleene logic
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• On the efficiency of subsumption algorithms
• Automated Reasoning
• Theory and Applications of Satisfiability Testing
• Automating Coherent Logic
• Fast theta-subsumption with constraint satisfaction algorithms

This page was built for publication: Subsumption Algorithms for Three-Valued Geometric Resolution