A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
From MaRDI portal
Publication:6653095
Cites work
- scientific article; zbMATH DE number 1641581 (Why is no real title available?)
- scientific article; zbMATH DE number 50150 (Why is no real title available?)
- scientific article; zbMATH DE number 605917 (Why is no real title available?)
- scientific article; zbMATH DE number 7552282 (Why is no real title available?)
- scientific article; zbMATH DE number 965572 (Why is no real title available?)
- A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
- A decidable quantified fragment of set theory involving ordered pairs with applications to description logics
- A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions
- Adding partial functions to constraint logic programming with sets
- An automatically verified prototype of the Android permissions system
- An automatically verified prototype of the Tokeneer ID station specification
- Automated proof of Bell-LaPadula security properties
- Automated reasoning with restricted intensional sets
- Automated verification of relational while-programs
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Decidability of ∀*∀‐Sentences in Membership Theories
- Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
- Efficient E-Matching for SMT Solvers
- Formal analysis of Android's permission-based security model
- From Computational Logic to Computational Biology
- Set unification
- Simplify: a theorem prover for program checking
- Solving quantified verification conditions using satisfiability modulo theories
- Solving quantifier-free first-order constraints over finite sets and binary relations
- THE DECISION PROBLEM FOR RESTRICTED UNIVERSAL QUANTIFICATION IN SET THEORY AND THE AXIOM OF FOUNDATION
- The Bernays-Schönfinkel-Ramsey class for set theory: decidability
- The Logically Simplest Form of the Infinity Axiom
- The calculus of relations as a foundation for mathematics
- Theorem proving using lazy proof explication.
- Truth In V for ∃*∀∀-Sentences is Decidable
- Undecidability results for restricted universally quantified formulae of set theory
- Verifying Android's permission model
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)
