Superposition for higher-order logic (Q6156638): Difference between revisions

@@ Property / cites work @@
+On connections and higher-order logic
@@ Property / cites work: On connections and higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Q2751353
@@ Property / cites work: Q2751353 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264723
@@ Property / cites work: Q4264723 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4989394
@@ Property / cites work: Q4989394 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition for full higher-order logic
@@ Property / cites work: Superposition for full higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with lambdas
@@ Property / cites work: Superposition with lambdas / rank @@
+Normal rank
@@ Property / cites work @@
+LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+A combinator-based superposition calculus for higher-order logic
+Normal rank
@@ Property / cites work @@
+The computability path ordering
@@ Property / cites work: The computability path ordering / rank @@
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / 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 @@
+A Linear Spine Calculus
@@ Property / cites work: A Linear Spine Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Types, tableaus, and Gödel's God
@@ Property / cites work: Types, tableaus, and Gödel's God / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with equivalence reasoning and delayed clause normal form transformation
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+A unification algorithm for typed \(\bar\lambda\)-calculus
+Normal rank
@@ Property / cites work @@
+Mechanizing \(\omega\)-order type theory through unification
+Normal rank
@@ Property / cites work @@
+Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
+Normal rank
@@ Property / cites work @@
+An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
+Normal rank
@@ Property / cites work @@
+Higher-order rewrite systems and their confluence
@@ Property / cites work: Higher-order rewrite systems and their confluence / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751358
@@ Property / cites work: Q2751358 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / 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
@@ Property / cites work @@
+Making higher-order superposition work
@@ Property / cites work: Making higher-order superposition work / rank @@
+Normal rank
@@ Property / cites work @@
+A comprehensive framework for saturation theorem proving
+Normal rank