scientific article; zbMATH DE number 4053062

MaRDI QIDQ3789101zbMATH OpenFDO

Authors Amy P. Felty, Dale Miller

Publication date 1988

zbMATH Keywords

pattern matchinglogic programminginference rulestheorem provershigher-order unification\(\lambda \) Prolog

Mathematics Subject Classification ID

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

Recommendations

• Implementing tactics and tacticals in a higher-order logic programming language
• Programming with higher-order logic.
• Higher-order Horn clauses
• scientific article; zbMATH DE number 3988745
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application

Cited in

(32)

• The practice of logical frameworks
• Theo: An interactive proof development system
• A framework for proof systems
• α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
• scientific article; zbMATH DE number 4049001 (Why is no real title available?)
• The foundation of a generic theorem prover
• Tactical theorem proving in program verification
• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• On extensibility of proof checkers
• Mechanized metatheory revisited
• Higher-order unification revisited: Complete sets of transformations
• Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
• scientific article; zbMATH DE number 5850137 (Why is no real title available?)
• scientific article; zbMATH DE number 4094864 (Why is no real title available?)
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
• Uniform proofs as a foundation for logic programming
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
• Proof-producing synthesis of ML from higher-order logic
• A treatment of higher-order features in logic programming
• Representing proof transformations for program optimization
• A proof procedure for the logic of hereditary Harrop formulas
• Unification under a mixed prefix
• Implementing tactics and tacticals in a higher-order logic programming language
• Implementing type theory in higher order constraint logic programming
• Focusing in Linear Meta-logic
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Higher-order unification with dependent function types
• Using typed lambda calculus to implement formal systems on a machine
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
• Program tactics and logic tactics
• scientific article; zbMATH DE number 3986671 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3789101)