Efficient full higher-order unification

DOI10.4230/LIPICS.FSCD.2020.5MaRDI QIDQ6854431zbMATH OpenFDO

Authors Petar Vukmirović, Alexander Bentkamp, Visa Nummelin

Publication date 24 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2020.5

zbMATH Keywords

theorem provingterm rewritinghigher-order logicunificationindexing data structures

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx) Computer science (68-XX)

Cites work

• scientific article; zbMATH DE number 3935004 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A unification algorithm for second-order monadic terms
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Efficient full higher-order unification
• Fingerprint indexing for paramodulation and rewriting
• Functions-as-constructors Higher-order Unification
• Higher-order unification revisited: Complete sets of transformations
• Higher-order unification via combinators
• Isabelle/HOL. A proof assistant for higher-order logic
• LEO-II and Satallax on the Sledgehammer test bench
• Mechanizing \(\omega\)-order type theory through unification
• Programming with higher-order logic.
• Regular patterns in second-order unification
• Restricted combinatory unification
• Satallax: An Automatic Higher-Order Prover
• Superposition with lambdas
• Superposition with structural induction
• The CADE-27 automated theorem proving system competition -- CASC-27
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• The higher-order prover Leo-III

Cited in

(1)

• Efficient full higher-order unification

This page was built for publication: Efficient full higher-order unification

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