Superposition modulo non-linear arithmetic

DOI10.1007/978-3-642-24364-6_9MaRDI QIDQ3172887zbMATH OpenOpenAlexFDO

Authors Andreas Eggers, E. V. Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach

Publication date 7 October 2011

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24364-6_9

Mathematics Subject Classification ID

Combined logics (03B62) Logic in computer science (03B70)

Recommendations

• Superposition modulo linear arithmetic SUP(LA)
• Theoretical Aspects of Computing – ICTAC 2005
• Integrating Linear Arithmetic into Superposition Calculus
• Superposition modulo a Shostak theory.
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions

Cites work

• scientific article; zbMATH DE number 1444347 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Conflict resolution for air traffic management: a study in multiagent hybrid systems
• Engineering DPLL(T) + Saturation
• Refutational theorem proving for hierarchic first-order theories
• Superposition for fixed domains
• Superposition modulo linear arithmetic SUP(LA)
• Superposition modulo non-linear arithmetic
• The Image Computation Problem in Hybrid Systems Model Checking

Cited in

(6)

• Superposition modulo linear arithmetic SUP(LA)
• An efficient subsumption test pipeline for BS(LRA) clauses
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Harald Ganzinger's legacy: contributions to logics and programming
• Superposition modulo non-linear arithmetic
• Superposition decides the first-order logic fragment over ground theories

Describes a project that uses

Uses Software

• ABsolver
• z3
• REDLOG
• SPASS

This page was built for publication: Superposition modulo non-linear arithmetic

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