Deduction by combining semantic tableaux and integer programming

DOI10.1007/3-540-61377-3_31MaRDI QIDQ6560161zbMATH OpenFDO

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)

Recommendations

• Publication:4863689
• Many-valued logic and mixed integer programming
• scientific article; zbMATH DE number 1552522
• Incremental theory reasoning methods for semantic tableaux
• Logic applied to integer programming and integer programming applied to logic

Cites work

• scientific article; zbMATH DE number 3177183 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• A structure-preserving clause form translation
• Computing definite logic programs by partial instantiation
• Many-valued logic and mixed integer programming
• SETHEO: A high-performance theorem prover

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)