Information Technology Reference
In-Depth Information
Sketching Some of the Remaining Features.
The resource distribution approach
means that most important functions
in the prover are given a resource argument: a bound for the number of “steps”;
they return the “current state” and the resource remainder. Resource exhaustion
is one of the flags for such a function to stop. The resource is distributed between
the goals according to the strategy heuristics. All this helps to automate the
tactics of proof, breaking off any unsuccessful proof branch when it grows too
long (recall that a generic “solving” task is algorithmically undecidable).
The inductive reasoning
is organized through adding of equalities (see,
for example, the materials on Inductive Prover (M.Clavel) at the Maude system
site).
The first approach strategy (FAS)
for the
formula proof by the given
theory
(the function
prove
) consists of transforming the list of
goals
,trying
in a certain sequence the inference
rules
(attempts) of Simplification (
ukbb
),
Constants Lemma, Implication Elimination, and Induction by expression value
(by
construction
of such value). The resource is distributed between the goals
in the simplest way (far from being optimal).
Examples of What It Can and Cannot Do:
the FAS strategy proves au-
tomatically, with small resource cost, such tasks as, for example, (1)
forall
[N,M] (N+M = M+N)
for the unary natural number arithmetics specified by re-
cursive definitions, (2)
reverse reverse xs = xs
for the list reverse defined
via concatenation, and the latter defined via
CONS
. But (2) needs a certain sim-
ple lemma to be introduced as a
hint
. For although FAS proves the lemma and
all the rest, it fails to guess to put this lemma as a subgoal. We intend to im-
prove FAS to the extent that it will become capable of tasks like proving the
equivalence of various sorting algorithms.
Early Future Plans:
to link the CA library to the prover (they are imple-
mented in the same language), move OL from many-sorted TRW to order-sorted,
add high-order operators, functoriality, develop AC completion, and develop fur-
ther strategies (e.g. with setting an ordering on the subgoal formulas, heuristics
for choosing the induction parameter) and special prover libraries (e.g. for the
polynomial algebra).
References
1. Goguen, J., Meseguer, J.: Order-Sorted Algebra I: Equational Deduction for Multi-
ple Inheritance, Polymorphism, and Partial Operations. (1988?).
http://citeseer.nj.nec.com/goguen92ordersorted.html
2. Hsiang, J.: Refutational theorem proving using term-rewriting systems. Artificial
Intelligence, 1985, v.
25
(255-300).
3. Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In Proc. of
14-th Conference on ALP, Karlsruhe, LNCS
267
, (54-71), 1987.
4. Huet, G., Oppen, D.: Equations and rewrite rules. A Survey. In “Formal languages:
perspectives an open problems” (349-405). New York, Pergamon Press, 1980
5. Knuth, D., Bendix, P.: Simple word problems in universal algebras. In “Computa-
tional Problems in Abstract Algebra”, (263-297), Pergamos Press, 1970.
6. Lochner, B., Hillenbrand, T.: A Phytography of Waldmeister. AI Communications,
IOS Press,
(15)
(2,3) (2002) (127-133).