A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers

Cites Work

Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
Title not available (Why is that?)
A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions
The calculus of relations as a foundation for mathematics
Solving quantified verification conditions using satisfiability modulo theories
Automated proof of Bell-LaPadula security properties
An automatically verified prototype of the Tokeneer ID station specification
Solving quantifier-free first-order constraints over finite sets and binary relations
Automated reasoning with restricted intensional sets
Verifying Android’s Permission Model
A Decidable Quantified Fragment of Set Theory Involving Ordered Pairs with Applications to Description Logics.
The Bernays-Schönfinkel-Ramsey class for set theory: decidability
Truth In V for ∃*∀∀-Sentences is Decidable
Set unification
Simplify: a theorem prover for program checking
Efficient E-Matching for SMT Solvers
Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
Undecidability results for restricted universally quantified formulae of set theory
THE DECISION PROBLEM FOR RESTRICTED UNIVERSAL QUANTIFICATION IN SET THEORY AND THE AXIOM OF FOUNDATION
Adding partial functions to Constraint Logic Programming with sets
Formal Analysis of Android's Permission-Based Security Model
The Logically Simplest Form of the Infinity Axiom
Decidability of ∀*∀‐Sentences in Membership Theories
Automated Verification of Relational While-Programs
Computer Aided Verification
An automatically verified prototype of the Android permissions system
A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
From Computational Logic to Computational Biology

This page was built for publication: A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers

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