Skip to content

Latest commit

 

History

History
5 lines (4 loc) · 268 Bytes

README.md

File metadata and controls

5 lines (4 loc) · 268 Bytes

Matching Logic Prover

  • prover contains the matching logic prover, implemented in the K framework.
  • checker contains the proof checkers of matching logic.
  • ml2fol contains a prototype translation from matching logic to first-order logic in smt2lib format.