Integrating Simplex with Tableaux
From MaRDI portal
Publication:3455763
DOI10.1007/978-3-319-24312-2_7zbMath1471.68304MaRDI 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
tableaux; linear arithmetic; branch-and-bound method; Coq; proof checking; Zenon; general simplex algorithm
03B35: Mechanization of proofs and logical operations
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Related Items
Uses Software
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