Automated reasoning with restricted intensional sets

DOI10.1007/s10817-021-09589-wOpenAlexW3147784962MaRDI QIDQ2666960

Maximiliano Cristiá, Gianfranco Rossi

Publication date: 23 November 2021

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

Full work available at URL: https://arxiv.org/abs/1910.09118

zbMATH Keywords

set theoryconstraint programming\(\{log\}\)set unificationintensional setsrestricted universal quantifiersetlog

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

An automatically verified prototype of the Android permissions system ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ Unnamed Item ⋮ An automatically verified prototype of the Tokeneer ID station specification

Uses Software

• TPTP
• Gringo
• MiniZinc
• ProB
• Z/EVES
• Z
• BWare
• JSetL
• SETL

Cites Work

• Unnamed Item
• 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
• A set solver for finite set relation algebra
• Automated proof of Bell-LaPadula security properties
• Separation logic with linearly compositional inductive predicates and set data constraints
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Solving quantifier-free first-order constraints over finite sets and binary relations
• A decision procedure for restricted intensional sets
• Abstract state machines, Alloy, B, TLA, VDM, and Z. 4th international conference, ABZ 2014, Toulouse, France, June 2--6, 2014. Proceedings
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• A Logic-Based Framework for Verifying Consensus Algorithms
• Logic programs with propositional connectives and aggregates
• {log}: A language for programming in logic with finite sets
• Set constructors in a logic database language
• Set unification
• A Constructive semantic characterization of aggregates in answer set programming
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Combining Theories with Shared Set Operations
• The B-Book
• Functional ASP with Intensional Sets: Application to Gelfond-Zhang Aggregates
• Abstract gringo
• 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
• A transformational approach to negation in logic programming
• Quantifier Instantiation Techniques for Finite Model Finding in SMT
• Logic Programming
• Exploiting Symmetry in SMT Problems
• On Bounded Reachability of Programs with Set Comprehensions
• Constructive negation and constraint logic programming with sets

This page was built for publication: Automated reasoning with restricted intensional sets