Implementing tactics and tacticals in a higher-order logic programming language
type: Item
instance of: scholarly article
title: Implementing tactics and tacticals in a higher-order logic programming language
zbMATH Open document ID: 0783.68117
DOI: 10.1007/BF00881900
published in: Journal of Automated Reasoning
publication date: 1994-01-23T00:00:00Z
Mathematics Subject Classification ID: 68T99
Mathematics Subject Classification ID: 68N17
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 484764
zbMATH Keywords: tactics
zbMATH Keywords: natural deduction
zbMATH Keywords: higher-order logic
zbMATH Keywords: logical frameworks
zbMATH Keywords: tacticals
zbMATH Keywords: proof systems
author: Amy P. Felty
describes a project that uses: Prolog
describes a project that uses: Nuprl
describes a project that uses: Elf
MaRDI profile type: Publication
cites work: A formulation of the simple theory of types
cites work: The calculus of constructions
cites work: Q3789101
cites work: Q4012881
cites work: Q4282512
cites work: A framework for defining logics
cites work: Q4722037
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Depth-first iterative-deepening: An optimal admissible tree search
cites work: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
cites work: Unification under a mixed prefix
cites work: Uniform proofs as a foundation for logic programming
cites work: Higher-order Horn clauses
cites work: The foundation of a generic theorem prover
cites work: Q4012879
cites work: Q5559220
cites work: Q5632554
cites work: Q3742689
full work available at URL: https://doi.org/10.1007/bf00881900
OpenAlex ID: W2076819871
description: scientific article; zbMATH DE number 484764