scientific article; zbMATH DE number 1303341

MaRDI QIDQ4249894zbMATH OpenFDO

Authors Michael Beeson

Publication date 7 November 1999

zbMATH Keywords

automated theorem provingcircumscriptionlambda calculusmost-general-unifier propertysecond-order logicunification algorithm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Recommendations

• Unification for -calculi without propagation rules
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• Delaying unification algorithms for lambda calculi
• On the confluence of lambda-calculus with conditional rewriting
• Logic and computation in a lambda calculus with intersection and union types
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
• Unification in an extensional lambda calculus with ordered function sorts and constant overloading
• Reduction and unification in lambda calculi with a general notion of subtype
• scientific article; zbMATH DE number 2044492
• scientific article; zbMATH DE number 3997190

Cited in

(8)

• Delaying unification algorithms for lambda calculi
• General E-unification with eager variable elimination and a nice cycle rule
• Unification via the s_e-style of explicit substitutions
• Unification for -calculi without propagation rules
• Analytic tableaux for higher-order logic with choice
• Automated Reasoning
• Automatic derivation of the irrationality of e
• A -unifiability test for set theory

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 Q4249894)