Superposition for Bounded Domains
From MaRDI portal
Publication:4913861
DOI10.1007/978-3-642-36675-8_4zbMath1383.03018OpenAlexW1897269102MaRDI QIDQ4913861
Th. Hillenbrand, Christoph Weidenbach
Publication date: 16 April 2013
Published in: Automated Reasoning and Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-36675-8_4
Related Items
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ An Extension of the Knuth-Bendix Ordering with LPO-Like Properties ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ SCL clause learning from simple models
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On deciding satisfiability by theorem proving with speculative inferences
- Computing finite models by reduction to function-free clause logic
- Labelled splitting
- Refutational theorem proving for hierarchic first-order theories
- Superposition as a decision procedure for timed automata
- Combination of Disjoint Theories: Beyond Decidability
- More SPASS with Isabelle
- The Hyper Tableaux Calculus with Equality and an Application to Finite Model Computation
- Solving SAT and SAT Modulo Theories
- Proof Systems for Effectively Propositional Logic
- The Isabelle Framework
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Superposition Modulo Linear Arithmetic SUP(LA)
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- New results on rewrite-based satisfiability procedures
- Theoretical Aspects of Computing – ICTAC 2005
- On the Saturation of YAGO
