IsaPlanner
Encyclopedia
IsaPlanner is a proof planner for the interactive proof assistant, Isabelle
. Originally developed by Lucas Dixon as part of his PhD thesis at the University of Edinburgh
, it is now maintained by members of the Mathematical Reasoning Group, in the School of Informatics
at Edinburgh.
IsaPlanner is the latest of a series of proof planners written at Edinburgh. Earlier planners include Clam and LambdaClam.
and proving
theorem
s. IsaPlanner works by manipulating reasoning states, records of open goals, the current proof plan and other important information, and combinators are functions mapping reasoning states to lazy lists
of successor reasoning states.
IsaPlanner's library supplies combinators for branching and iteration
, amongst other tasks, and powerful reasoning techniques can be created by combining simpler reasoning techniques with these combinators.
Several reasoning techniques come ready implemented within IsaPlanner, notably, IsaPlanner features an implementation of dynamic rippling
, a rippling heuristic
capable of working in higher order
settings, a best-first rippling heuristic and a reasoning technique for proofs by induction
.
Additional features include an interactive tracing tool, for manually stepping through proof attempts and a module for viewing and manipulating hierarchical proofs.
expressions
as opposed to functional
expressions, again suitable for use in higher order domains, and integration of IsaPlanner with Proof General.
Isabelle theorem prover
The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic theorem prover. It is an LCF-style theorem prover , so it is based on a small logical core guaranteeing logical correctness...
. Originally developed by Lucas Dixon as part of his PhD thesis at the University of Edinburgh
University of Edinburgh
The University of Edinburgh, founded in 1583, is a public research university located in Edinburgh, the capital of Scotland, and a UNESCO World Heritage Site. The university is deeply embedded in the fabric of the city, with many of the buildings in the historic Old Town belonging to the university...
, it is now maintained by members of the Mathematical Reasoning Group, in the School of Informatics
University of Edinburgh School of Informatics
The School of Informatics is an academic unit of the University of Edinburgh, in Scotland, responsible for research, teaching, outreach and commercialisation in Informatics....
at Edinburgh.
IsaPlanner is the latest of a series of proof planners written at Edinburgh. Earlier planners include Clam and LambdaClam.
Features
IsaPlanner allows the user to encode reasoning techniques, using a combinator language, for conjecturingConjecture
A conjecture is a proposition that is unproven but is thought to be true and has not been disproven. Karl Popper pioneered the use of the term "conjecture" in scientific philosophy. Conjecture is contrasted by hypothesis , which is a testable statement based on accepted grounds...
and proving
Mathematical proof
In mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...
theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s. IsaPlanner works by manipulating reasoning states, records of open goals, the current proof plan and other important information, and combinators are functions mapping reasoning states to lazy lists
Lazy evaluation
In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...
of successor reasoning states.
IsaPlanner's library supplies combinators for branching and iteration
Iteration
Iteration means the act of repeating a process usually with the aim of approaching a desired goal or target or result. Each repetition of the process is also called an "iteration," and the results of one iteration are used as the starting point for the next iteration.-Mathematics:Iteration in...
, amongst other tasks, and powerful reasoning techniques can be created by combining simpler reasoning techniques with these combinators.
Several reasoning techniques come ready implemented within IsaPlanner, notably, IsaPlanner features an implementation of dynamic rippling
Rippling
Rippling refers to a group of meta-level heuristics, developed primarily in the Mathematical Reasoning Group in the School of Informatics at the University of Edinburgh, and most commonly used to guide inductive proofs in automated theorem proving systems...
, a rippling heuristic
Heuristic
Heuristic refers to experience-based techniques for problem solving, learning, and discovery. Heuristic methods are used to speed up the process of finding a satisfactory solution, where an exhaustive search is impractical...
capable of working in higher order
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
settings, a best-first rippling heuristic and a reasoning technique for proofs by induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
.
Additional features include an interactive tracing tool, for manually stepping through proof attempts and a module for viewing and manipulating hierarchical proofs.
Planned features
Features currently being implemented, or planned for the future, are an expanded set of proof critics, suitable for use in higher order domains, dynamic relational rippling, a rippling heuristic suitable for rippling over relationalRelation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
expressions
Expression (mathematics)
In mathematics, an expression is a finite combination of symbols that is well-formed according to rules that depend on the context. Symbols can designate numbers , variables, operations, functions, and other mathematical symbols, as well as punctuation, symbols of grouping, and other syntactic...
as opposed to functional
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
expressions, again suitable for use in higher order domains, and integration of IsaPlanner with Proof General.