Safe Haskell  None 

Language  Haskell2010 
 getSubGoals :: [F] > [F]
 getRefutes :: [F] > [F]
 getAxioms :: [F] > [F]
 getConjeture :: [F] > Maybe F
 printPreamble :: String > IO ()
 printAuxSignatures :: ProofMap > [ProofTree] > IO ()
 printSubGoals :: [F] > F > String > IO ()
 printProofBody :: [F] > F > String > [F] > String > IO ()
 printProofWhere :: ProofMap > ProofTree > IO ()
 buildProofMap :: [F] > ProofMap
 buildProofTree :: ProofMap > F > ProofTree
 parseFile :: Maybe FilePath > IO [F]
How to use tstp2agda
Let use an example, given this problem
$ cat problem.tstp fof(a1,axiom,a). fof(a2,conjecture,a).
and the corresponding Metis proof
$ cat proof.tstp  SZS status Theorem for examplesproblemTest1.tstp SZS output start CNFRefutation for examplesproblemTest1.tstp fof(a1, axiom, (a)). fof(a2, conjecture, (a)). fof(subgoal_0, plain, (a), inference(strip, [], [a2])). fof(negate_0_0, plain, (~ a), inference(negate, [], [subgoal_0])). fof(normalize_0_0, plain, (~ a), inference(canonicalize, [], [negate_0_0])). fof(normalize_0_1, plain, (a), inference(canonicalize, [], [a1])). fof(normalize_0_2, plain, ($false), inference(simplify, [], [normalize_0_0, normalize_0_1])). cnf(refute_0_0, plain, ($false), inference(canonicalize, [], [normalize_0_2])). SZS output end CNFRefutation for examplesproblemTest1.tstp
we create some requiered data structures
main ∷ IO () main = do  read the file formulas ←parseFile
"proof.tstp"  create a map proofmap ←buildProofMap
formulas  get subgoals,refutes,axioms, and the conjecture let subgoals =getSubGoals
formulas let refutes =getRefutes
formulas let axioms =getAxioms
formulas let (Just conj) =getConjeture
formulas  build aproofTree
for each subgoal (using his associated refute) let prooftree =map
(buildProofTree
proofmap) refutes
and then print the actual Agda code
 PREAMBLE: module definitions and importsprintPreamble
"BaseProof"  STEP 1: Print auxiliary functionsprintAuxSignatures
proofmap prooftree  STEP 2: Subgoal handlingprintSubGoals
subgoals conj "goals"  STEP 3: Print main function signatureprintProofBody
axioms conj "proof" subgoals "goals"  STEP 4: Print all the step of the proof as local definitionsmapM_
(printProofWhere
proofmap prooftree
and then get
module BaseProof where open import Data.FOL.Shallow postulate funnormalize00 : { a : Set} → ¬ a → ¬ a postulate funnormalize01 : { a : Set} → a → a postulate funnormalize02 : { a : Set} → ¬ a → a → ⊥ postulate funrefute00 : ⊥ → ⊥ postulate goals : { a : Set} → a → a proof : { a : Set} → a → a proof {a} a1 = goals subgoal0 where funnegate00 : ¬ a → ⊥ funnegate00 negate00 = refute00 where normalize00 = funnormalize00 negate00 normalize01 = funnormalize01 a1 normalize02 = funnormalize02 normalize00 normalize01 refute00 = funrefute00 normalize02 subgoal0 = proofByContradiction funnegate00
Getters
getSubGoals :: [F] > [F]
Extract subgoals from a list of formulae.
getRefutes :: [F] > [F]
Extract refuting steps from a list of formulae.
getConjeture :: [F] > Maybe F
Try to extract a conjecture from a list of formulae and checks for uniqueness.
Agda translation
Print a series of auxiliary functions required to perform most
of the steps of the proof. Every Formula
has a corresponding
function which has its parents as arguments and the current
function as return value. Since a proof is split in various
subgoals, this function receives a list of subProofTree
s
funstepₘ_ₙ : { ν₀ ... νᵢ : Set } → stepₘ_ₙ₁ → ... → stepₘ_ₙⱼ → stepₘ_ₙ
Print the main subgoal implication function
subGoalImplName : subgoal₀ → ... → subgoalₙ → conjecture
:: [F]  Axioms 
> F  Conjecture 
> String  Function name ( 
> [F]  Subgoals 
> String  Name of 
> IO () 
Print main proof type signature, and top level LHS ans RHS of the form
proofName : axiom₀ → ... → axiomₙ → conjecture proofName axiomName₀ ... axiomNameₙ = subGoalImplName subgoal₀ ... subgoalₙ where
printProofWhere :: ProofMap > ProofTree > IO ()
For a given subgoal print each formula definition in reverse order of dependencies
negation₀ : ¬ τ₀ → ⊥ negation₀ negate₀ = refute₀ where step₀_ᵢ = funstep₀_ᵢ step₀_ᵢ₁ .. step₀_ᵢⱼ ... step₀_₀ = funstep₀_₀ step₀_₀₁ .. step₀_₀ₖ subgoal₀ = proofByContradiction negation₀ ... negationₙ : ¬ τₙ → ⊥ negationₙ negateₙ = refuteₙ where stepₙ_ₜ = funstepₙ_ₜ stepₙ__ₜ₁ .. stepₙ_ₜₒ ... stepₙ_₀ = funstepₙ_₀ stepₙ_₀₁ .. stepₙ_₀ᵤ subgoal₀ = proofByContradiction negationₙ
This is perhaps the most important step and the one that does the
"actual" proof translation. The basic principle is to define each
subgoal
in terms of its parents which for most (if not all) cases
implies a negation
of the subgoal
and a corresponding refute
term.
buildProofMap
lf
, given a list of functions lf
builds a ProofMap
:: ProofMap 

> F  Root formula 
> ProofTree  Tree of formulas with the given formula as root 
buildProofTree
m
f
, build a ProofTree
with f
as root,
and using m
for dependencies resolution. Depending on the root,
not all values in m
are used.