Integrating Simplex with Tableaux

DOI10.1007/978-3-319-24312-2_7zbMath1471.68304OpenAlexW2266110381MaRDI QIDQ3455763

David Delahaye, Guillaume Bury

Publication date: 11 December 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal-mines-paristech.archives-ouvertes.fr/hal-01215490/file/zen-ari.pdf

zbMATH Keywords

tableauxlinear arithmeticbranch-and-bound methodCoqproof checkingZenongeneral simplex algorithm

Mathematics Subject Classification ID

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

Related Items (1)

First-order automated reasoning with theories: when deduction modulo theory meets practice

Uses Software

• Coq
• TPTP
• z3
• Zenon
• CVC4
• BWare

Cites Work

• Theorem proving modulo
• Autarkic computations in formal proofs
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• The B-Book
• Hierarchic Superposition with Weak Abstraction
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

This page was built for publication: Integrating Simplex with Tableaux