Metis-based Paramodulation Tactic for HOL Light. Färber, M. & Kaliszyk, C. In GCAI 2015. Global Conference on Artificial Intelligence Metis-based, volume 36, pages 127--136, 2015.
abstract   bibtex   
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. 1
@inproceedings{Farber2015,
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. 1},
author = {F{\"{a}}rber, Michael and Kaliszyk, Cezary},
booktitle = {GCAI 2015. Global Conference on Artificial Intelligence Metis-based},
file = {:Users/jonaprieto/Mendeley/F{\"{a}}rber, Kaliszyk - 2015 - Metis-based Paramodulation Tactic for HOL Light.pdf:pdf},
pages = {127--136},
title = {{Metis-based Paramodulation Tactic for HOL Light}},
volume = {36},
year = {2015}
}

Downloads: 0