(LIA) - Model Evolution with Linear Integer Arithmetic Constraints

DOI10.1007/978-3-540-89439-1_19zbMath1182.03033OpenAlexW1509261266MaRDI QIDQ5505559

Alexander Fuchs, Cesare Tinelli, Peter Baumgartner

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)

Related Items

Superposition Modulo Non-linear Arithmetic, Axiomatic Constraint Systems for Proof Search Modulo Theories, Superposition as a decision procedure for timed automata, Superposition decides the first-order logic fragment over ground theories, Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories, Linear Quantifier Elimination as an Abstract Decision Procedure, Model Evolution with Equality Modulo Built-in Theories