bookmarks  1

  •  

    IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. The system provides an interactive tracing tool that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being used with Isabelle and Proof General) It is based on the Isabelle theorem prover and the Isar language. The main proof technique written in IsaPlanner is an inductive theorem prover based on Rippling. This is applicable within Isabelle's Higher Order Logic, and can easily be adapted to Isabelle's other logics. The system now the main platform for proof planning research in the Edinburgh mathematical reasoning group
    13 years ago by @draganigajic
    (0)
     
     
  • ⟨⟨
  • 1
  • ⟩⟩

publications  

    No matching posts.
  • ⟨⟨
  • ⟩⟩