SAT-Inspired Higher-Order Eliminations (Q6135757): Difference between revisions

@@ Property / cites work @@
+Superposition for full higher-order logic
@@ Property / cites work: Superposition for full higher-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Rewrite-based Equational Theorem Proving with Selection and Simplification
+Normal rank
@@ Property / cites work @@
+Q4249891
@@ Property / cites work: Q4249891 / rank @@
+Normal rank
@@ Property / cites work @@
+A combinator-based superposition calculus for higher-order logic
+Normal rank
@@ Property / cites work @@
+Q2723442
@@ Property / cites work: Q2723442 / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / 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 @@
+Efficient CNF Simplification Based on Binary Implication Graphs
+Normal rank
@@ Property / cites work @@
+Predicate Elimination for Preprocessing in First-Order Theorem Proving
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+SCAN—Elimination of predicate quantifiers
@@ Property / cites work: SCAN—Elimination of predicate quantifiers / 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 @@
+Extensional higher-order paramodulation in Leo-III
+Normal rank
@@ Property / cites work @@
+The CADE-28 Automated Theorem Proving System Competition – CASC-28
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / 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 @@
+SAT-Inspired Eliminations for Superposition
@@ Property / cites work: SAT-Inspired Eliminations for Superposition / rank @@
+Normal rank