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:

https://pastebin.com/KvnLidiz

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

https://pastebin.com/Cj3FBmtw

To get the ivy proof I did this:

prover9 -f ex1.in > 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.