Deduction by combining semantic tableaux and integer programming

DOI10.1007/3-540-61377-3_31zbMATH Open1540.68257MaRDI QIDQ6560161FDOQ6560161

Authors: Bernhard Beckert, Reiner Hähnle 

Publication date: 21 June 2024

Mathematics Subject Classification ID

Integer programming (90C10) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Title not available (Why is that?)
• A structure-preserving clause form translation
• SETHEO: A high-performance theorem prover
• Title not available (Why is that?)
• Many-valued logic and mixed integer programming
• Computing definite logic programs by partial instantiation

This page was built for publication: Deduction by combining semantic tableaux and integer programming

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