Superposition modulo a Shostak theory.

DOI10.1007/B11829MaRDI QIDQ5900718zbMATH OpenOpenAlexFDO

Authors Harald Ganzinger, Th. Hillenbrand, Uwe Waldmann

Publication date 20 April 2010

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

Full work available at URL https://doi.org/10.1007/b11829

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Recommendations

• Superposition modulo linear arithmetic SUP(LA)
• Superposition for Fixed Domains
• Superposition for fixed domains
• Theoretical Aspects of Computing – ICTAC 2005
• Modular proof systems for partial functions with Evans equality

Cited in

(9)

• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Canonization for disjoint unions of theories
• Superposition for fixed domains
• Superposition modulo non-linear arithmetic
• Superposition for Fixed Domains
• scientific article; zbMATH DE number 881986 (Why is no real title available?)
• Superposition for bounded domains
• Harald Ganzinger's legacy: contributions to logics and programming
• Automated Reasoning

This page was built for publication: Superposition modulo a Shostak theory.

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