
LambdaClam
 Referenced in 24 articles
[sw19614]
 LambdaClam ( λclam, lclam) is a proof planning system that support proof planning over higherorder ... domains: System description: Proof planning in higherorder logic with λClam. This system description outlines ... λClam system for proof planning in higherorder logic. The usefulness and feasibility of applying ... higherorder 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]
 higherorder 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. Speedwise, 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 proofofconcept 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...