Restricted combinatory unification

DOI10.1007/978-3-030-29436-6_5OpenAlexW2969261745MaRDI QIDQ2305407

Giles Reger, Ahmed Bhayat

Publication date: 10 March 2020

Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/restricted-combinatory-unification(fef710fb-aa70-4a19-808e-bd0d80288d4a).html

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Extensional higher-order paramodulation in Leo-III, Unnamed Item, Unnamed Item, The CADE-27 Automated theorem proving System Competition – CASC-27, Superposition with lambdas, Making higher-order superposition work, Making higher-order superposition work, A combinator-based superposition calculus for higher-order logic, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective

Uses Software

• VAMPIRE
• TPTP
• Satallax
• StarExec
• E Theorem Prover
• Leo-III
• CoqHammer

Cites Work

• Unnamed Item
• Unnamed Item
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Theorem proving modulo
• Hammer for Coq: automation for dependent type theory
• Superposition with structural induction
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Superposition for \(\lambda\)-free higher-order logic
• The higher-order prover Leo-III
• Higher-order unification revisited: Complete sets of transformations
• Higher order unification via explicit substitutions
• Higher-order unification via combinators
• Decidability of bounded higher-order unification
• Translating higher-order clauses to first-order clauses
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
• Satallax: An Automatic Higher-Order Prover
• Higher-order term indexing using substitution trees
• Embedding Deduction Modulo into a Prover
• Term Rewriting and All That
• Substitution tree indexing
• Decidable higher-order unification problems
• Automated Reasoning
• Functions-as-constructors Higher-order Unification
• Superposition with lambdas