A combinator-based superposition calculus for higher-order logic (Q2096452): 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 @@
+Extending SMT solvers to higher-order logic
@@ Property / cites work: Extending SMT solvers to higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with lambdas
@@ Property / cites work: Superposition with lambdas / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition for \(\lambda\)-free higher-order logic
+Normal rank
@@ Property / cites work @@
+The higher-order prover \textsc{Leo}-II
@@ Property / cites work: The higher-order prover \textsc{Leo}-II / rank @@
+Normal rank
@@ Property / cites work @@
+Restricted combinatory unification
@@ Property / cites work: Restricted combinatory unification / rank @@
+Normal rank
@@ Property / cites work @@
+A Knuth-Bendix-like ordering for orienting combinator equations
+Normal rank
@@ Property / cites work @@
+Expressing Polymorphic Types in a Many-Sorted Language
+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 @@
+Hammer for Coq: automation for dependent type theory
+Normal rank
@@ Property / cites work @@
+Q3522248
@@ Property / cites work: Q3522248 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012178
@@ Property / cites work: Q4012178 / rank @@
+Normal rank
@@ Property / cites work @@
+A Focused Sequent Calculus for Higher-Order Logic
@@ Property / cites work: A Focused Sequent Calculus for Higher-Order Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Translating higher-order clauses to first-order clauses
+Normal rank
@@ Property / cites work @@
+A compact representation of proofs
@@ Property / cites work: A compact representation of proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751359
@@ Property / cites work: Q2751359 / rank @@
+Normal rank
@@ Property / cites work @@
+Unification with abstraction and theory instantiation in saturation-based reasoning
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+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
@@ Property / cites work @@
+Q5028439
@@ Property / cites work: Q5028439 / rank @@
+Normal rank