(LIA) - Model Evolution with Linear Integer Arithmetic Constraints

DOI10.1007/978-3-540-89439-1_19zbMATH Open1182.03033OpenAlexW1509261266MaRDI QIDQ5505559FDOQ5505559

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

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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)