Integrating simplex with tableaux

DOI10.1007/978-3-319-24312-2_7MaRDI QIDQ3455763zbMATH OpenOpenAlexFDO

Authors Guillaume Bury, David Delahaye

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

Coqtableauxbranch-and-bound methodlinear arithmeticproof 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)

Recommendations

• A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
• Integrating Linear Arithmetic into Superposition Calculus
• Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL
• Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover
• scientific article; zbMATH DE number 4112064

Cites work

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

Cited in

(2)

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

Describes a project that uses

Uses Software

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

This page was built for publication: Integrating simplex with tableaux

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