Using meta-level inference for selective application of multiple rewrite rule sets in algebraic manipulation
Artificial IntelligencePublished 1 May 1981
Alan Bundy, Bob Welham
Citations100
SJR quartileQ1
SJR score1.84
SNIP3.30
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A technique for controlling inference, meta-level inference, and a program for algebraic manipulation, PRESS, which embodies this technique, is described.
Abstract
In this paper we describe a technique for controlling inference, called meta-level inference, and a program for algebraic manipulation, PRESS, which embodies this technique. In PRESS, algebraic expressions are manipulated by a series of methods. The appropriate method is chosen by meta-level inference and itself uses meta-level reasoning to select and apply rewrite rules to the current expression. The use of meta-level inference is shown to drastically cut down on search, lead to clear and modular programs, aid the proving of properties of the program and enable the automatic learning of both new algebraic facts and new control information.
Keywords
Computer Science
Simple Word Problems in Universal Algebras
1,373 Citations1983Donald E. Knuth, PETER B. BENDIX
Journal of the ACMConfluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
1,074 Citations1980Gérard Huet
This paper gives new results, and presents old ones, concerning ChurchRosser theorems for rewrmng systems, depending solely on axioms for a binary relatton called reduction, and how these criteria yield new methods for the mechanizaUon of equattonal theories.
Artificial IntelligenceProlegomena to a theory of mechanized formal reasoning
368 Citations1980Richard W. Weyhrauch
This is an informal description of my ideas about using formal logic as a tool for reasoning systems using computers, illustrated by the features of FOL.
Communications of the ACMAlgebraic simplification
138 Citations1971Joel Moses
The spectrum of approaches to the design of automatic simplification capabilities in an algebraic manipulation system is delineated, and several positive results about the existence of powerful simplification algorithms and the number-theoretic conjectures on which they rely are described.
International Joint Conference on Artificial IntelligenceMeta-level knowledge: overview and applications
123 Citations1977Randall Davis, Bruce C. Buchanan
The concept of meta-level Knowledge is defined, and four examples of applications to tasks such as transfer of expertise from a domain expert to a program, and the maintenance and use of large Knowledge bases are reviewed.
The MACSYMA system
118 Citations1971William A. Martin, Richard J. Fateman
MACSYMA is a system for symbolic manipulation of algebraic expressions which is being developed at Project MAC and makes extensive use of the power of its rational function subsystem.
Mathematical Foundations of Computer ScienceComputation and Deduction.
116 Citations1973Patrick J. Hayes
This work proposes a nanozyme colorimetric sensor for the specific carbosulfan detection, based on its distinctive hydrolysis property, and sheds light on the role of metal-based or metal-free nanozyme among analytical applications.
Conflunt reductions: Abstract properties and applications to term rewriting systems
90 Citations1977Gérard Huet
This paper gives new results, and presents old ones in a unified formalism, concerning Church-Rosser theorems for rewriting systems, and shows how these results yield efficient methods for the mechanization of equational theories.
Artificial IntelligenceTowards the automation of set theory and its logic
32 Citations1978Frank M. Brown
A prototype extensible deductive system for elementary set theory which is based on truth-value preserving transformations is described and an experimental application of it to the first few chapters of W. V. O. Quine's book: Set Theory and its Logic.
Journal of the ACMProving Theorems about LISP Functions
30 Citations1975Robert S. Boyer, J Strother Moore
Some simple heuristics combining evaluation and mathematical induction are described which are implemented in a program that automatically proves a wide variety of theorems about recursive LISP functions.
International Joint Conference on Artificial IntelligenceAnalyzing mathematical proofs (or reading between the lines)
13 Citations1975Alan Bundy
Analysis of equation solving and analysis of the solutions of experienced mathematicians reveals a system of high-level descriptions, strategies and goals, which can be used to guide the search through an explosively large search space.
Artificial IntelligenceA man-machine theorem-proving system
11 Citations1974W. W. Bledsoe, Peter Bruell
A man-machine theorem proving system at the University of Texas (Austin) which has been used to prove a few theorems in general topology, built around a modified form of IMPLY, a natural-deduction-like theorem proving technique.