Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. MUNCH - Automated Reasoner for Sets and Multisets
 
conference paper

MUNCH - Automated Reasoner for Sets and Multisets

Piskac, Ruzica  
•
Kuncak, Viktor  orcid-logo
Giesl, Juergen
•
Haehnle, Reiner
2010
Proceedings of the 5th International Joint Conference on Automated Reasoning
International Joint Conference on Automated Reasoning

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

PiskacKuncak10MUNCHAutomatedReasonerforSets.pdf

Access type

openaccess

Size

220.61 KB

Format

Adobe PDF

Checksum (MD5)

dd4e555d7938d47769696a2066d4bb1d

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés