Making higher-order superposition work (Q5918575): Difference between revisions

@@ Property / describes a project that uses @@
+DISCOUNT
@@ Property / describes a project that uses: DISCOUNT / 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 @@
+TPTP
@@ Property / describes a project that uses: TPTP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Why3
@@ Property / describes a project that uses: Why3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC4
@@ Property / describes a project that uses: CVC4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Zipperposition
@@ Property / describes a project that uses: Zipperposition / rank @@
+Normal rank
@@ 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 @@
+HOLyHammer
@@ Property / describes a project that uses: HOLyHammer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VAMPIRE
@@ Property / describes a project that uses: VAMPIRE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+StarExec
@@ Property / describes a project that uses: StarExec / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+WhyML
@@ Property / describes a project that uses: WhyML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Satallax
@@ Property / describes a project that uses: Satallax / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Sledgehammer
@@ Property / describes a project that uses: Sledgehammer / 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 / 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-021-09613-z
+Normal rank
@@ Property / OpenAlex ID @@
+W4206463158
@@ Property / OpenAlex ID: W4206463158 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4255513
@@ Property / cites work: Q4255513 / rank @@
+Normal rank
@@ Property / cites work @@
+Analytic tableaux for higher-order logic with choice
+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 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 @@
+Superposition for \(\lambda\)-free higher-order logic
+Normal rank
@@ Property / cites work @@
+Logic for Programming, Artificial Intelligence, and Reasoning
+Normal rank
@@ Property / cites work @@
+Restricted combinatory unification
@@ Property / cites work: Restricted combinatory unification / rank @@
+Normal rank
@@ Property / cites work @@
+A combinator-based superposition calculus for higher-order logic
+Normal rank
@@ Property / cites work @@
+Reducing higher-order theorem proving to a sequence of SAT problems
+Normal rank
@@ Property / cites work @@
+Hammer for Coq: automation for dependent type theory
+Normal rank
@@ Property / cites work @@
+A unifying splitting framework
@@ Property / cites work: A unifying splitting framework / rank @@
+Normal rank
@@ Property / cites work @@
+Internal Guidance for Satallax
@@ Property / cites work: Internal Guidance for Satallax / rank @@
+Normal rank
@@ Property / cites work @@
+Why3 — Where Programs Meet Provers
@@ Property / cites work: Why3 — Where Programs Meet Provers / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-19
@@ Property / cites work: Automated Deduction – CADE-19 / rank @@
+Normal rank
@@ Property / cites work @@
+Layered clause selection for theory reasoning (short paper)
+Normal rank
@@ Property / cites work @@
+Completeness in the theory of types
@@ Property / cites work: Completeness in the theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Selecting the Selection
@@ Property / cites work: Selecting the Selection / 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 @@
+Q3685171
@@ Property / cites work: Q3685171 / rank @@
+Normal rank
@@ Property / cites work @@
+HOL(y)Hammer: online ATP service for HOL Light
@@ Property / cites work: HOL(y)Hammer: online ATP service for HOL Light / rank @@
+Normal rank
@@ Property / cites work @@
+Q5581665
@@ Property / cites work: Q5581665 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3863048
@@ Property / cites work: Q3863048 / rank @@
+Normal rank
@@ Property / cites work @@
+Completely non-clausal theorem proving
@@ Property / cites work: Completely non-clausal theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Q2751358
@@ Property / cites work: Q2751358 / rank @@
+Normal rank
@@ Property / cites work @@
+Superposition with first-class booleans and inprocessing clausification
+Normal rank
@@ Property / cites work @@
+Purely Functional Data Structures
@@ Property / cites work: Purely Functional Data Structures / rank @@
+Normal rank
@@ Property / cites work @@
+Playing with AVATAR
@@ Property / cites work: Playing with AVATAR / rank @@
+Normal rank
@@ Property / cites work @@
+Q3150301
@@ Property / cites work: Q3150301 / rank @@
+Normal rank
@@ Property / cites work @@
+Faster, higher, stronger: E 2.3
@@ Property / cites work: Faster, higher, stronger: E 2.3 / rank @@
+Normal rank
@@ Property / cites work @@
+Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
+Normal rank
@@ Property / cites work @@
+Q4557854
@@ Property / cites work: Q4557854 / rank @@
+Normal rank
@@ Property / cites work @@
+There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners
+Normal rank
@@ Property / cites work @@
+Extensional higher-order paramodulation in Leo-III
+Normal rank
@@ Property / cites work @@
+LEO-II and Satallax on the Sledgehammer test bench
+Normal rank
@@ Property / cites work @@
+The CADE-14 ATP system competition
@@ Property / cites work: The CADE-14 ATP system competition / 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 @@
+The CADE-27 Automated theorem proving System Competition – CASC-27
+Normal rank
@@ Property / cites work @@
+The 10th IJCAR automated theorem proving system competition – CASC-J10
+Normal rank
@@ Property / cites work @@
+Another algorithm for bracket abstraction
@@ Property / cites work: Another algorithm for bracket abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+AVATAR: The Architecture for First-Order Theorem Provers
+Normal rank
@@ Property / cites work @@
+Q5028439
@@ Property / cites work: Q5028439 / rank @@
+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
@@ Property / cites work @@
+Effective Normalization Techniques for HOL
@@ Property / cites work: Effective Normalization Techniques for HOL / rank @@
+Normal rank