A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
type: Item
instance of: scholarly article
title: A practical decision procedure for quantifier-free, decidable languages extended with restricted quantifiers
author: Maximiliano Cristiá
author: Gianfranco Rossi
published in: Journal of Automated Reasoning
publication date: 2024-12-16T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7958429
zbMATH Keywords: restricted quantifiers
zbMATH Keywords: set theory
zbMATH Keywords: constraint logic programming
zbMATH Keywords: \(\{Log\}\)
MaRDI profile type: Publication
cites work: Truth In V for ∃*∀∀-Sentences is Decidable
cites work: Automated Verification of Relational While-Programs
cites work: Formal Analysis of Android's Permission-Based Security Model
cites work: Verifying Android’s Permission Model
cites work: Q5691140
cites work: Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
cites work: Q3999861
cites work: A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions
cites work: A decidable quantified fragment of set theory involving ordered pairs with applications to description logics
cites work: Q2740887
cites work: An automatically verified prototype of the Android permissions system
cites work: Solving quantifier-free first-order constraints over finite sets and binary relations
cites work: Automated proof of Bell-LaPadula security properties
cites work: Automated reasoning with restricted intensional sets
cites work: An automatically verified prototype of the Tokeneer ID station specification
cites work: Q5087785
cites work: From Computational Logic to Computational Biology
cites work: A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
cites work: Adding partial functions to Constraint Logic Programming with sets
cites work: Efficient E-Matching for SMT Solvers
cites work: Simplify: a theorem prover for program checking
cites work: Set unification
cites work: Computer Aided Verification
cites work: Solving quantified verification conditions using satisfiability modulo theories
cites work: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
cites work: The calculus of relations as a foundation for mathematics
cites work: Decidability of ∀*∀‐Sentences in Membership Theories
cites work: The Bernays-Schönfinkel-Ramsey class for set theory: decidability
cites work: Undecidability results for restricted universally quantified formulae of set theory
cites work: The Logically Simplest Form of the Infinity Axiom
cites work: THE DECISION PROBLEM FOR RESTRICTED UNIVERSAL QUANTIFICATION IN SET THEORY AND THE AXIOM OF FOUNDATION
cites work: Q4301167
DOI: 10.1007/S10817-024-09713-6
description: scientific article; zbMATH DE number 7958429