MUNCH - Automated Reasoner for Sets and Multisets (System Description)

paper ps   
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.

Citation

Ruzica Piskac and Viktor Kuncak. Munch - automated reasoner for sets and multisets (system description). In IJCAR, 2010.

BibTex Entry

@inproceedings{PiskacKuncak10MUNCHAutomatedReasonerforSets,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {MUNCH - Automated Reasoner for Sets and Multisets (System Description)},
  booktitle = {IJCAR},
  abstract = {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.},
  year = 2010
}