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

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

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)