Safe Haskell	None
Language	Haskell2010

T2A

Contents

How to use tstp2agda
Getters
Agda translation
TSTP parsing

Synopsis

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 examplesproblemTest-1.tstp
  SZS output start CNFRefutation for examplesproblemTest-1.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 examplesproblemTest-1.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 a proofTree for each subgoal (using his associated refute)
  let prooftree = map (buildProofTree proofmap) refutes

and then print the actual Agda code

  -- PREAMBLE: module definitions and imports
  printPreamble "BaseProof"
  -- STEP 1: Print auxiliary functions
  printAuxSignatures proofmap prooftree
  -- STEP 2: Subgoal handling
  printSubGoals subgoals conj "goals"
  -- STEP 3: Print main function signature
  printProofBody axioms conj "proof" subgoals "goals"
  -- STEP 4: Print all the step of the proof as local definitions
  mapM_ (printProofWhere proofmap  prooftree

and then get

  module BaseProof where
  open import Data.FOL.Shallow
  postulate fun-normalize-0-0 : { a : Set} → ¬ a → ¬ a
  postulate fun-normalize-0-1 : { a : Set} → a → a
  postulate fun-normalize-0-2 : { a : Set} → ¬ a → a → ⊥
  postulate fun-refute-0-0 :  ⊥ → ⊥
  postulate goals : { a : Set} → a → a
  proof : { a : Set} → a → a
  proof {a} a1 = goals subgoal-0
    where
      fun-negate-0-0 : ¬ a → ⊥
      fun-negate-0-0 negate-0-0 = refute-0-0
        where
          normalize-0-0 = fun-normalize-0-0 negate-0-0
          normalize-0-1 = fun-normalize-0-1 a1
          normalize-0-2 = fun-normalize-0-2 normalize-0-0 normalize-0-1
          refute-0-0 = fun-refute-0-0 normalize-0-2
      subgoal-0 = proofByContradiction fun-negate-0-0

Getters

getSubGoals :: [F] -> [F]

Extract subgoals from a list of formulae.

getRefutes :: [F] -> [F]

Extract refuting steps from a list of formulae.

getAxioms :: [F] -> [F]

Extract axioms 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

printPreamble

Arguments

:: String	Module name
-> IO ()

printAuxSignatures

Arguments

:: ProofMap	map of formulas
-> [ProofTree]	list of subgoals
-> IO ()

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 sub-ProofTrees

   fun-stepₘ_ₙ : { ν₀ ... νᵢ : Set } → stepₘ_ₙ₁ → ... → stepₘ_ₙⱼ → stepₘ_ₙ

printSubGoals

Arguments

:: [F]	Subgoals
-> F	Conjecture
-> String	Function name (`subGoalImplName`)
-> IO ()

Print the main subgoal implication function

  subGoalImplName : subgoal₀ → ... → subgoalₙ → conjecture

printProofBody

Arguments

:: [F]	Axioms
-> F	Conjecture
-> String	Function name (`proofName`)
-> [F]	Subgoals
-> String	Name of `subGoalImplName`
-> 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₀_ᵢ = fun-step₀_ᵢ step₀_ᵢ₁ .. step₀_ᵢⱼ
          ...
          step₀_₀ = fun-step₀_₀ step₀_₀₁ .. step₀_₀ₖ
      subgoal₀ = proofByContradiction negation₀
      ...
      negationₙ : ¬ τₙ → ⊥
      negationₙ negateₙ = refuteₙ
        where
          stepₙ_ₜ = fun-stepₙ_ₜ stepₙ__ₜ₁ .. stepₙ_ₜₒ
          ...
          stepₙ_₀ = fun-stepₙ_₀ 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

Arguments

:: [F]	List of functions
-> ProofMap	Map of the given functions indexed by its names

buildProofMap lf, given a list of functions lf builds a ProofMap

buildProofTree

Arguments

:: ProofMap	`Map` for resolving dependencies
-> 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.

TSTP parsing

parseFile :: Maybe FilePath -> IO [F]

Similar to parse but reading directly from a file or stdin.