(LIA) - Model Evolution with Linear Integer Arithmetic Constraints

DOI10.1007/978-3-540-89439-1_19MaRDI QIDQ5505559zbMATH OpenOpenAlexFDO

Authors Peter Baumgartner, Alexander Fuchs, Cesare Tinelli

Publication date 27 January 2009

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-89439-1_19

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Model Evolution with Equality Modulo Built-in Theories
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Automated Deduction – CADE-20
• Model evolution with equality -- revised and implemented
• Integrating Linear Arithmetic into Superposition Calculus

Cited in

(9)

• Axiomatic constraint systems for proof search modulo theories
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Superposition modulo non-linear arithmetic
• Superposition as a decision procedure for timed automata
• Superposition decides the first-order logic fragment over ground theories
• Symbolic Model Construction for Saturated Constrained Horn Clauses
• Model Evolution with Equality Modulo Built-in Theories
• Linear quantifier elimination as an abstract decision procedure
• ALASCA: reasoning in quantified linear arithmetic

This page was built for publication: (LIA) - Model Evolution with Linear Integer Arithmetic Constraints

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