Translating higher-order clauses to first-order clauses (Q2471742): Difference between revisions

@@ Property / describes a project that uses @@
+E Theorem Prover
@@ Property / describes a project that uses: E Theorem Prover / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OTTER
@@ Property / describes a project that uses: OTTER / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Metis_
@@ Property / describes a project that uses: Metis_ / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Jahob
@@ Property / describes a project that uses: Jahob / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-007-9085-y
+Normal rank
@@ Property / OpenAlex ID @@
+W1979623128
@@ Property / OpenAlex ID: W1979623128 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q57382631
@@ Property / Wikidata QID: Q57382631 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical induction in Otter-lambda
@@ Property / cites work: Mathematical induction in Otter-lambda / rank @@
+Normal rank
@@ Property / cites work @@
+Logic for Programming, Artificial Intelligence, and Reasoning
+Normal rank
@@ Property / cites work @@
+Using First-Order Theorem Provers in the Jahob Data Structure Verification System
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4809048
@@ Property / cites work: Q4809048 / rank @@
+Normal rank
@@ Property / cites work @@
+Director strings as combinators
@@ Property / cites work: Director strings as combinators / rank @@
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Automation for interactive proof: first prototype
@@ Property / cites work: Automation for interactive proof: first prototype / rank @@
+Normal rank
@@ Property / cites work @@
+Unification under a mixed prefix
@@ Property / cites work: Unification under a mixed prefix / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Source-Level Proof Reconstruction for Interactive Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q4692880
@@ Property / cites work: Q4692880 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2778806
@@ Property / cites work: Q2778806 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4539622
@@ Property / cites work: Q4539622 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+Another algorithm for bracket abstraction
@@ Property / cites work: Another algorithm for bracket abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+A new implementation technique for applicative languages
+Normal rank
@@ Property / cites work @@
+Q2751379
@@ Property / cites work: Q2751379 / rank @@
+Normal rank
@@ Property / DBLP publication ID @@
+journals/jar/MengP08
@@ Property / DBLP publication ID: journals/jar/MengP08 / rank @@
+Normal rank