scientific article

zbMath0645.68097MaRDI QIDQ3789101

Amy P. Felty, Dale A. Miller

Publication date: 1988

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

pattern matchinglogic programminghigher-order unificationinference rulestheorem provers\(\lambda \) Prolog

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) General topics in the theory of software (68N01)

Related Items (19)

Higher-order unification with dependent function types ⋮ Uniform proofs as a foundation for logic programming ⋮ Program tactics and logic tactics ⋮ On extensibility of proof checkers ⋮ Focusing in Linear Meta-logic ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Unification under a mixed prefix ⋮ Theo: An interactive proof development system ⋮ A framework for proof systems ⋮ Tactical theorem proving in program verification ⋮ Representing proof transformations for program optimization ⋮ The foundation of a generic theorem prover ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ Implementing type theory in higher order constraint logic programming ⋮ Mechanized metatheory revisited ⋮ α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic ⋮ Implementing tactics and tacticals in a higher-order logic programming language ⋮ A proof procedure for the logic of hereditary Harrop formulas ⋮ The practice of logical frameworks

Uses Software

• Nuprl

This page was built for publication: