Re: Anon Thread for June 6 2020

by BlakeKeiller, Sunday, June 21, 2020, 19:45 (532 days ago) @ BlakeKeiller

Here is some lisp code that is able to convert some ivy proofs into the proofgold assembly format:

It works on this simple example, which I had in the file

To get the ivy proof I did this:

prover9 -f > ex1.out

prooftrans ivy -f ex1.out > ex1.ivy

To convert to a proofgold document, I loaded the lisp code and then did this:

(ivy-to-pfg "ex1.ivy" "ex1.pfg")

This created a file ex1.pfg that contains the theorem and proof in the HOHF theory. The code can also make a document in the empty theory by first setting *theory* to nil.

(setq *theory* nil)
(ivy-to-pfg "ex1.ivy" "ex1empty.pfg")

The lisp code does not yet handle equational reasoning (e.g., FLIP and PARAMOD) and may not handle the most general resolution cases, but it's a start.

Complete thread:

 RSS Feed of thread

powered by my little forum