• Lambda-Clam

  • Referenced in 24 articles [sw19614]
  • LambdaClam ( λclam, lclam) is a proof planning system that support proof planning over higher-order ... domains: System description: Proof planning in higher-order logic with λClam. This system description outlines ... λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying ... higher-order proof planning to a number of types of problem is outlined, in particular...
  • IsaPlanner

  • Referenced in 30 articles [sw02047]
  • IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle ... that allows you to interact the proof planning attempt. (see the screenshot of IsaPlanner being...
  • OMEGA

  • Referenced in 32 articles [sw19623]
  • higher-order logic based on proof planning...
  • LOUI

  • Referenced in 10 articles [sw19627]
  • browser with hypertext facilities, proof and proof plan presentation in natural language, and an editor...
  • EXPANDER

  • Referenced in 6 articles [sw22715]
  • restricted application areas and implement specific proof plans, strategies or tactics. It is written ... SML/NJ. EXPANDER executes single inference steps. Each proof is a sequence of goal sets...
  • CoCLAM

  • Referenced in 2 articles [sw28719]
  • based on the idea of proof planning. Proof planning constructs the higher level steps ... control the proof search. Part of proof planning involves the use of failure information ... Haskell. We have developed a proof plan for coinduction and a critic associated with this ... proof plan. These have been implemented in CoCLAM, an extended version of CLAM, with encouraging...
  • PROVERB

  • Referenced in 4 articles [sw29672]
  • also prove to be useful for proof planning and proving by analogy...
  • MPTP

  • Referenced in 26 articles [sw02489]
  • version generates about 30000 problems from complete proofs of Mizar theorems, and about 630000 problems ... system, their solutions, current limitations, and planned future extensions. We present results of first experiments ... also describe first implementation of the Mizar Proof Advisor (MPA) used for selecting suitable axioms...
  • Plastic

  • Referenced in 18 articles [sw07403]
  • various extensions, in the form of a proof assistant. Typed LF is a framework type ... test ideas from Durham research, and we plan to use it as a platform ... interface, courtesy of David Aspinall’s generic Proof General. Speed-wise, it compares favourably with...
  • Tecton

  • Referenced in 9 articles [sw28905]
  • hypertext links; and automating substantial parts of proofs through rewriting, induction, case analysis, and generalization ... procedure. Further development of the system is planned as part of an overall framework aimed...
  • Teyjus

  • Referenced in 16 articles [sw21364]
  • manipulate formal objects such as formulas, programs, proofs and types. Towards harnessing these benefits, methods ... these ideas has recently been completed. The planned presentation will exhibit this system—called Teyjus...
  • DISCOUNT

  • Referenced in 14 articles [sw19613]
  • Competition between multiple strategies, combined with reactive planning, reuslts in an adaptation of the whole ... control strategies based on learning from previous proof experiences. One of these strategies forms...
  • TorchLight

  • Referenced in 4 articles [sw13534]
  • planning benchmarks, in particular pertaining to the complete absence of local minima. The proofs...
  • Mentoniezh

  • Referenced in 6 articles [sw32254]
  • solving. Its main original feature is a plan recognition method which deduces, from the student ... problem, the student’s intended proof. That enables the student to be provided with context...
  • UTP2

  • Referenced in 5 articles [sw06342]
  • simple theory of designs with some proof extracts is used to illustrate the above features ... with a discussion of current limitations and planned improvements to the tool...
  • Prooftree

  • Referenced in 1 article [sw17593]
  • getting lost between different subgoals in interactive proof development. It clearly shows where the current ... thus helps in developing the right plan for solving it. Prooftree uses different colors ... proven subgoals, the current branch in the proof and the still open subgoals. Sequent texts...
  • Saoithin

  • Referenced in 4 articles [sw06341]
  • simple theory of designs with some proof extracts is used to illustrate the above features ... with a discussion of current limitations and planned improvements to the tool...
  • ProofScript

  • Referenced in 2 articles [sw22724]
  • ProofScript: proof scripting for the masses. The goal of the ProofPeer project is to make ... reality. An important part of our plan to make this happen is ProofScript, a language ... each other to produce formal definitions and proofs. All aspects of ProofScript are shaped...
  • Billie

  • Referenced in 1 article [sw27246]
  • customized visual representations of designed buildings and planned constructions. With reusable and exchangeable visualization configurations ... with a prototypical implementation: Billie is a proof-of-concept framework written in Java that...
  • webLurch

  • Referenced in 2 articles [sw20925]
  • check the steps in students’ mathematical proofs. Users write in a natural language, but mark ... features, among others. We conclude with design plans for ongoing development of the web version...