MUNCH - Automated Reasoner for Sets and Multisets

This system description provides an overview of the MUNCH reasoner for sets and multisets. MUNCH takes as the input a formula in a logic that supports expressions about sets, multisets, and integers. Constraints over collections and integers are connected using the cardinality operator. Our logic is a fragment of logics of popular interactive theorem provers, and MUNCH is the first fully automated reasoner for this logic. MUNCH reduces input formulas to equisatisfiable linear integer arithmetic formulas. MUNCH reasoner is publicly available. It is implemented in the Scala programming language and currently uses the SMT solver Z3 to solve the generated integer linear arithmetic constraints.


Editeur(s):
Giesl, Juergen
Haehnle, Reiner
Publié dans:
Proceedings of the 5th International Joint Conference on Automated Reasoning, 149-155
Présenté à:
International Joint Conference on Automated Reasoning, Edinburgh, UK, July 16-19, 2010
Année
2010
Publisher:
Springer
Mots-clefs:
Laboratoires:




 Notice créée le 2010-12-01, modifiée le 2019-08-12

n/a:
Télécharger le document
PDF

Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)