Access the full text.
Sign up today, get DeepDyve free for 14 days.
Loading next page...
/lp/springer-journals/implementing-tactics-and-tacticals-in-a-higher-order-logic-programming-8vpxKeDtM5
References (47)
-
R. Harper, F. Honsell, G. Plotkin (1993)
A framework for defining logicsJ. ACM, 40
-
D. Miller, G. Nadathur, F. Pfenning, A. Scedrov (1991)
Uniform Proofs as a Foundation for Logic ProgrammingAnn. Pure Appl. Log., 51
-
(1990)
eLP, a Common Lisp Implementation of Prolog -
Furió, Honselly, Gordon, PlotkinzAbstractThe (1987)
A Framework for De ning LogicsRobert Harper -
(1989)
Higher-order uni cation with dependent types. In Rewriting Tech- niques and Applications, pages 121{136 -
A. Felty (1991)
A Logic Programming Approach to Implementing Higher-Order Term Rewriting -
R. Constable, S. Allen, Mark Bromley, R. Cleaveland, J. Cremer, R. Harper, Douglas Howe, Todd Knoblock, N. Mendler, P. Panangaden, James Sasaki, Scott Smith (1986)
Implementing mathematics with the Nuprl proof development system -
D. Prawitz (1971)
Ideas and Results in Proof TheoryStudies in logic and the foundations of mathematics, 63
-
Gerhard Gentzen (1969)
The Collected Papers of Gerhard Gentzen -
Philippa Gardner (1992)
Representing logics in type theory -
D. Miller, G. Nadathur (1987)
A Logic Programming Approach to Manipulating Formulas and Programs -
A. Church (1940)
A formulation of the simple theory of typesJournal of Symbolic Logic, 5
-
G. Nadathur, B. Jayaraman (1989)
Towards a WAM model for ?Prolog -
(1984)
Intuitionistic Type Theory, Studies in Proof Theory, Lecture Notes. BIBLIOPOLIS -
M. Gordon (1979)
Edinburgh LCF: A mechanised logic of computation -
(1965)
Dag Prawitz. Natural Deduction. Almqvist & Wiksell -
E. KorfRichard (1985)
Depth-first iterative-deepening: an optimal admissible tree searchArtificial Intelligence
-
G. Huet (1975)
A Unification Algorithm for Typed lambda-CalculusTheor. Comput. Sci., 1
-
L. Sterling, E. Shapiro (1986)
The Art of Prolog - Advanced Programming Techniques -
F. Pfenning, Conal Elliott (1988)
Higher-order abstract syntax -
(1935)
Investigations into logical deductions -
D. Miller (1992)
Unification Under a Mixed PrefixJ. Symb. Comput., 14
-
Conal Elliott, F. Pfenning (1990)
A Semi-Functional Implementation of a Higher-Order Logic Programming Language -
(1988)
Gbrard, 'The calculus of constructions', Information and Computation -
D. Miller (1991)
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification -
S. Dietzen, F. Pfenning (2004)
Higher-order and modal logic as a framework for explanation-based generalizationMachine Learning, 9
-
Olivier RidouxzyENAC, E. Belin, Toulouse Cedexpbrisset (1992)
The Architecture of an Implementation of Prolog : Prolog / Mali -
M. Hagiya (1990)
Programming by Example and Proving by Example Using Higher-order Unification -
G. Nadathur, D. Miller (1990)
Higher-order Horn clausesJ. ACM, 37
-
F. Dick (1980)
A survey of the project Automath -
A. Felty, D. Miller (1988)
Specifying Theorem Provers in a Higher-Order Logic Programming Language -
A. Felty, D. Miller (1989)
Specifying and implementing theorem provers in a higher-order logic programming language -
(1979)
A Mechanised Logic of Computation, Lecture Notes in Computer Science, Vol -
Gérard Huet (1975)
A unification algorithm for typed ?-calculusTheoretical Computer Science, 1
-
F. Pfenning (1991)
Logic programming in the LF logical framework -
G. Nadathur (1987)
A higher-order logic as the basis for logic programming -
A. Felty (1991)
A Logic Program for Transforming Sequent Proofs to Natural Deduction Proofs -
(1989)
A meta language for functional programs -
(1980)
Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp -
T. Coquand, G. Huet (1988)
The Calculus of ConstructionsInf. Comput., 76
-
R. Pareschi, D. Miller (1990)
Extending Definite Clause Grammars with Scoping Constructs -
A. Felty (1991)
Encoding dependent types in an intuitionistic logic -
Conal Elliott (1989)
Higher-order Unification with Dependent Function Types -
M. Gordon (1985)
HOL : A machine oriented formulation of higher order logic -
Lawrence Paulson (1989)
The foundation of a generic theorem proverJournal of Automated Reasoning, 5
-
D. Bruijn (1980)
A survey of the project AutomathStudies in logic and the foundations of mathematics, 133
-
Dag Prawitz (1965)
Natural Deduction
- Publisher
- Springer Journals
- Copyright
- Copyright
- Subject
- Computer Science; Mathematical Logic and Formal Languages; Artificial Intelligence; Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation
- ISSN
- 0168-7433
- eISSN
- 1573-0670
- DOI
- 10.1007/BF00881900
- Publisher site
- See Article on Publisher Site
Abstract
We argue that a logic programming language with a higher-order intuitionistic logic as its foundation can be used both to naturally specify and implement tactic-style theorem provers. The language extends traditional logic programming languages by replacing first-order terms with simply-typed λ-terms, replacing first-order unification with higher-order unification, and allowing implication and universal quantification in queries and the bodies of clauses. Inference rules for a variety of inference systems can be naturally specified in this language. The higher-order features of the language contribute to a concise specification of provisos concerning variable occurrences in formulas and the discharge of assumptions present in many inference systems. Tactics and tacticals, which provide a framework for high-level control over search for proofs, can be directly and naturally implemented in the extended language. This framework serves as a starting point for implementing theorem provers and proof systems that can integrate many diversified operations on formulas and proofs for a variety of logics. We present an extensive set of examples that have been implemented in the higher-order logic programming language λProlog.
Journal
Journal of Automated Reasoning – Springer Journals
Published: Dec 10, 2004