Decidable \({\exists}^{\forall}^\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420): Difference between revisions

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

Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420): Difference between revisions

Latest revision as of 21:15, 16 December 2024

Statements

Identifiers

Sitelinks

Mathematics(1 entry)

Decidable \({\exists}^{\forall}^\) first-order fragments of linear rational arithmetic with uninterpreted predicates (Q2031420): Difference between revisions