Solving quantifier-free first-order constraints over finite sets and binary relations

DOI10.1007/s10817-019-09520-4zbMath1468.03009OpenAlexW2939708371WikidataQ128119540 ScholiaQ128119540MaRDI QIDQ2303241

Maximiliano Cristiá, Gianfranco Rossi

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09520-4

zbMATH Keywords

set constraintsautomated theorem provingbinary relationssatisfiability solverset-relation algebra

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (9)

Automated reasoning with restricted intensional sets ⋮ An automatically verified prototype of the Android permissions system ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages ⋮ Complexity assessments for decidable fragments of set theory. II: A taxonomy for `small' languages involving membership ⋮ Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case* ⋮ Unnamed Item ⋮ Automated proof of Bell-LaPadula security properties ⋮ An automatically verified prototype of the Tokeneer ID station specification

Uses Software

• Coq
• RelView
• Alloy
• Isabelle/HOL
• TPTP
• Why3
• Prover9
• Mace4
• Cardinal
• ProB
• Kodkod
• CPGraph
• Z/EVES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A decidable two-sorted quantified fragment of set theory with ordered pairs and some undecidable extensions
• Constraint logic programming with a relational machine
• Interval propagation to reason about sets: Definition and implementation of a practical language
• Decision procedures for elementary sublanguages of set theory: XI. Multilevel syllogistic extended by some elementary map constructs
• The calculus of relations as a foundation for mathematics
• Cardinal: a finite sets constraint solver
• Relational semigroupoids: abstract relation-algebraic interfaces for finite relations between infinite types
• Isabelle/HOL. A proof assistant for higher-order logic
• Automated deduction -- CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6--11, 2017. Proceedings
• Relational constraint solving in SMT
• A decision procedure for restricted intensional sets
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• {log}: A language for programming in logic with finite sets
• Set unification
• On Automating the Calculus of Relations
• Decision problems for equational theories of relation algebras
• Adding partial functions to Constraint Logic Programming with sets
• A Decision Procedure for Sets, Binary Relations and Partial Functions
• System description generating models by SEM
• Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
• Automated Verification of Relational While-Programs
• Kodkod: A Relational Model Finder

This page was built for publication: Solving quantifier-free first-order constraints over finite sets and binary relations