Decision procedures using model building techniques

DOI10.1007/3-540-61377-3_35zbMath1540.03022MaRDI QIDQ6560165

Nicolas Peltier, Ricardo Caferra

Publication date: 21 June 2024

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• A method for simultaneous search for refutations and models by equational constraint solving
• Resolution methods for the decision problem
• Experiments with semantic paramodulation
• Proof theory in the USSR 1925–1969
• Resolution Strategies as Decision Procedures
• Using resolution for deciding solvable classes and building finite models
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Decision procedures using model building techniques