Restricted combinatory unification
From MaRDI portal
Recommendations
- Higher-order unification via combinators
- Permutative rewriting and unification
- scientific article; zbMATH DE number 4096777
- scientific article; zbMATH DE number 3945372
- Bounded combinatory logic
- scientific article; zbMATH DE number 4112560
- Selective Unification in (Constraint) Logic Programming*
- First-order unification by structural recursion
- scientific article; zbMATH DE number 4049096
- Bounded combinatory logic and lower complexity
Cites work
- scientific article; zbMATH DE number 1189058 (Why is no real title available?)
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Automated Reasoning
- Decidability of bounded higher-order unification
- Decidable higher-order unification problems
- Embedding Deduction Modulo into a Prover
- Extensional paramodulation for higher-order logic and its effective implementation Leo-III
- Functions-as-constructors Higher-order Unification
- Hammer for Coq: automation for dependent type theory
- Higher order unification via explicit substitutions
- Higher-order term indexing using substitution trees
- Higher-order unification revisited: Complete sets of transformations
- Higher-order unification via combinators
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
- Satallax: An Automatic Higher-Order Prover
- Substitution tree indexing
- Superposition for -free higher-order logic
- Superposition with lambdas
- Superposition with structural induction
- Term Rewriting and All That
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- The higher-order prover Leo-III
- Theorem proving modulo
- Translating higher-order clauses to first-order clauses
Cited in
(14)- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Extensional higher-order paramodulation in Leo-III
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Unification via the s_e-style of explicit substitutions
- A combinator-based superposition calculus for higher-order logic
- Making higher-order superposition work
- Superposition with lambdas
- Higher-order unification via combinators
- An empirical assessment of progress in automated theorem proving
- scientific article; zbMATH DE number 7471678 (Why is no real title available?)
- The CADE-27 automated theorem proving system competition -- CASC-27
- Making higher-order superposition work
- Extending a high-performance prover to higher-order logic
Describes a project that uses
Uses Software
This page was built for publication: Restricted combinatory unification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2305407)
