Experimenting with Deduction Modulo (Q5200022): Difference between revisions

@@ Property / cites work @@
+λν, a calculus of explicit substitutions which preserves strong normalisation
+Normal rank
@@ Property / cites work @@
+Term rewriting for normalization by evaluation.
@@ Property / cites work: Term rewriting for normalization by evaluation. / rank @@
+Normal rank
@@ Property / cites work @@
+A Semantic Completeness Proof for TaMeD
@@ Property / cites work: A Semantic Completeness Proof for TaMeD / 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 @@
+Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
+Normal rank
@@ Property / cites work @@
+Regaining cut admissibility in deduction modulo using abstract completion
+Normal rank
@@ Property / cites work @@
+Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
+Normal rank
@@ Property / cites work @@
+Polarized Resolution Modulo
@@ Property / cites work: Polarized Resolution Modulo / rank @@
+Normal rank
@@ Property / cites work @@
+HOL-λσ: an intentional first-order expression of  higher-order logic
+Normal rank
@@ Property / cites work @@
+Theorem proving modulo
@@ Property / cites work: Theorem proving modulo / rank @@
+Normal rank
@@ Property / cites work @@
+Term Rewriting and Applications
@@ Property / cites work: Term Rewriting and Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Q4524770
@@ Property / cites work: Q4524770 / rank @@
+Normal rank
@@ Property / cites work @@
+iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
+Normal rank
@@ Property / cites work @@
+Q3150300
@@ Property / cites work: Q3150300 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank