Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
From MaRDI portal
Publication:2031420
DOI10.1007/s10817-020-09567-8OpenAlexW3042291487MaRDI QIDQ2031420
Publication date: 9 June 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09567-8
first-order arithmeticBernays-Schönfinkel-Ramsey fragmentdifference constraintscombinations of theorieslinear rational arithmetic
Related Items (1)
Uses Software
Cites Work
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Theoretical Aspects of Computing - ICTAC 2004
- Theory and Applications of Satisfiability Testing
- Computer Aided Verification
- On Hierarchical Reasoning in Combinations of Theories
- On the Saturation of YAGO
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- Definability and decision problems in arithmetic
- Verification, Model Checking, and Abstract Interpretation
- Formal Methods at the Crossroads. From Panacea to Foundational Support
- Automated Deduction – CADE-19
- Ivy
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- YAGO2: a spatially and temporally enhanced knowledge base from Wikipedia
- On the complexity of quantified linear systems
- Decision procedures. An algorithmic point of view
- A new polynomial-time algorithm for linear programming
- Combining nonstably infinite theories
- Deciding effectively propositional logic using DPLL and substitution sets
- Computing finite models by reduction to function-free clause logic
- Decidable fragments of many-sorted logic
- Combination of convex theories: modularity, deduction completeness, and explanation
- The complexity of linear problems in fields
- Complexity, convexity and combinations of theories
- Complexity results for classes of quantificational formulas
- The monadic theory of order
- The computational complexity of logical theories
- A theory of timed automata
- Symbolic model checking for real-time systems
- Refutational theorem proving for hierarchic first-order theories
- Computational complexity and constraint logic programming languages
- The Bernays-Schönfinkel-Ramsey fragment with bounded difference constraints over the reals is decidable
- Solving quantified linear arithmetic by counterexample-guided instantiation
- A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications
- Property-directed inference of universal invariants or proving their absence
- Finite presentations of infinite structures: Automata and interpretations
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Superposition as a decision procedure for timed automata
- Superposition decides the first-order logic fragment over ground theories
- Theory combination: beyond equality sharing
- The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT
- Revisiting enumerative instantiation
- Strategies for combining decision procedures
- On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
- Modularity results for interpolation, amalgamation and superamalgamation
- Two variable first-order logic over ordered domains
- On Interpolation and Symbol Elimination in Theory Extensions
- Non-cyclic Sorts for First-Order Satisfiability
- EPR-Based Bounded Model Checking at Word Level
- The Bernays-Schönfinkel-Ramsey class for set theory: decidability
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
- BDI: a new decidable clause class
- Applying Linear Quantifier Elimination
- Combining Theories: The Ackerman and Guarded Fragments
- Superposition Modulo Non-linear Arithmetic
- Satisfiability Modulo Theories
- Model Checking Real-Time Systems
- Verification of Hybrid Systems
- A Gentle Non-disjoint Combination of Satisfiability Procedures
- Decidability and essential undecidability
- Weak Second‐Order Arithmetic and Finite Automata
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
- Decidable Fragments of Many-Sorted Logic
- Proof Systems for Effectively Propositional Logic
- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Superposition Modulo Linear Arithmetic SUP(LA)
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Combining Theories with Shared Set Operations
- Building a Calculus of Data Structures
- Deciding Combinations of Theories
- Simplification by Cooperating Decision Procedures
- Polynomial algorithms in linear programming
- Khachiyan’s algorithm for linear programming
- Presburger arithmetic with unary predicates is Π11 complete
- On languages with two variables
- Deciding First-Order Satisfiability when Universal and Existential Variables are Separated
- Superposition for Bounded Domains
- Planning with Effectively Propositional Logic
- On Combinations of Local Theory Extensions
- Hierarchic Superposition with Weak Abstraction
- On the Complexity of the Bernays-Schönfinkel Class with Datalog
- A comprehensive combination framework
- New results on rewrite-based satisfiability procedures
- Computer Aided Verification
- Computer Aided Verification
- Verification of Timed Automata via Satisfiability Checking
- Automated Deduction – CADE-20
- Modular reasoning about heap paths via effectively propositional formulas
- What Else Is Decidable about Integer Arrays?
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Frontiers of Combining Systems
This page was built for publication: Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
