Implementing tactics and tacticals in a higher-order logic programming language

This publication has 21 references indexed in Scilit:

• A logic program for transforming sequent proofs to natural deduction proofs
  Published by Springer Nature ,2006
• A logic programming approach to implementing higher-Order term rewriting
  Published by Springer Nature ,2005
• A framework for defining logics
  Journal of the ACM, 1993
• Encoding dependent types in an intuitionistic logic
  Published by Cambridge University Press (CUP) ,1991
• Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization
  Published by Elsevier ,1989
• The calculus of constructions
  Information and Computation, 1988
• Depth-first iterative-deepening
  Artificial Intelligence, 1985
• Edinburgh LCF
  Lecture Notes in Computer Science, 1979
• A unification algorithm for typed λ-calculus
  Theoretical Computer Science, 1975
• A formulation of the simple theory of types
  The Journal of Symbolic Logic, 1940