scientific article; zbMATH DE number 4053062

zbMATH Open0645.68097MaRDI QIDQ3789101FDOQ3789101

Authors: Amy P. Felty, Dale Miller 

Publication date: 1988

Title of this publication is not available (Why is that?)

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

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)

Cited In (32)

• Theo: An interactive proof development system
• α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
• A framework for proof systems
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• 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
• Representing proof transformations for program optimization
• A treatment of higher-order features in logic programming
• A proof procedure for the logic of hereditary Harrop formulas
• Implementing type theory in higher order constraint logic programming
• Implementing tactics and tacticals in a higher-order logic programming language
• Unification under a mixed prefix
• Focusing in Linear Meta-logic
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Higher-order unification with dependent function types
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
• Using typed lambda calculus to implement formal systems on a machine
• Title not available (Why is that?)
• Program tactics and logic tactics
• The practice of logical frameworks

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)