Restricted combinatory unification (Q2305407): Difference between revisions

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