Abstract

Metis is an automated theorem prover based on ordered paramodulation. It is widely employed in the interactive theorem provers Isabelle/HOL and HOL4 to automate proofs as well as reconstruct proofs found by automated provers. For both these purposes, the tableaux-based MESON tactic is frequently used in HOL Light. However, paramodulation-based provers such as Metis perform better on many problems involving equality. We created a Metis-based tactic in HOL Light which translates HOL problems to Metis, runs an OCaml version of Metis, and reconstructs proofs in Metis’ paramodulation calculus as HOL proofs. We evaluate the performance of Metis as proof reconstruction method in HOL Light.

BibTeX

@inproceedings{GCAI2015:Metis-based_Paramodulation_Tactic_for_HOL_Light,
  author    = "Michael Farber and Cezary Kaliszyk",
  title     = "Metis-based Paramodulation Tactic for {HOL} Light",
  booktitle = "Proceedings of the 1st Global Conference on Artificial
               Intelligence (GCAI 2015)",
  series    = "EPiC Series in Computing",
  volume    = 36,
  pages     = "127-136",
  year      = 2015
}