An online proof-producing decision procedure for mixed-integer linear arithmetic

DOI10.1007/3-540-36577-X_38MaRDI QIDQ4417953zbMATH OpenFDO

Authors Vijay Ganesh, David L. Dill, Sergey Berezin

Publication date 30 July 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2619/26190521.htm

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• CVC: A cooperating validity checker
• Complete integer decision procedures as derived rules in HOL
• An effective decision procedure for linear arithmetic over the integers and reals
• scientific article; zbMATH DE number 4112064
• A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic

Cited in

(6)

• Cutting the mix
• Cutting to the chase.
• Producing proofs from an arithmetic decision procedure in elliptical LF
• Satisfiability modulo theories
• Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
• Complete integer decision procedures as derived rules in HOL

Describes a project that uses

Uses Software

• Chaff
• CVC

This page was built for publication: An online proof-producing decision procedure for mixed-integer linear arithmetic

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