A decision procedure for sets, binary relations and partial functions

DOI10.1007/978-3-319-41528-4_10MaRDI QIDQ4633533zbMATH OpenOpenAlexWikidataFDO

Authors Maximiliano Cristiá, Gianfranco Rossi

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-41528-4_10

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Decision procedures for elementary sublanguages of set theory: XI. Multilevel syllogistic extended by some elementary map constructs
• Decision procedures for elementary sublanguages of set theory. XV: Multilevel syllogistic extended by the predicate Finite and the operators singleton and \(pred_ <\)
• A decision procedure for restricted intensional sets
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Decision procedures for elementary sublanguages of set theory VIII. A semidecision procedure for finite satisfiability of unqualified set-theoretic formulae

Cited in

(9)

• Handling transitive relations in first-order automated reasoning
• Solving quantifier-free first-order constraints over finite sets and binary relations
• Decision procedures for theories of sets with measures
• A decision procedure for restricted intensional sets
• Automated reasoning with restricted intensional sets
• Decision functions and characterization of their properties
• Reasoning with finite sets and cardinality constraints in SMT
• scientific article; zbMATH DE number 6130163 (Why is no real title available?)
• scientific article; zbMATH DE number 7552282 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle/HOL
• Cardinal
• Z/EVES
• Coq

This page was built for publication: A decision procedure for sets, binary relations and partial functions

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