System Description: E.T. 0.1 (Q3454109): Difference between revisions

@@ Property / describes a project that uses @@
+MPTP
@@ Property / describes a project that uses: MPTP / 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 @@
+Mizar
@@ Property / describes a project that uses: Mizar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MML
@@ Property / describes a project that uses: MML / 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 @@
+SigmaKEE
@@ Property / describes a project that uses: SigmaKEE / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+BliStr
@@ Property / describes a project that uses: BliStr / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SRASS
@@ Property / describes a project that uses: SRASS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MPTP 0.2
@@ Property / describes a project that uses: MPTP 0.2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MaSh
@@ Property / describes a project that uses: MaSh / 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 @@
+Flyspeck
@@ Property / describes a project that uses: Flyspeck / 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/978-3-319-21401-6_27
+Normal rank
@@ Property / OpenAlex ID @@
+W1413051680
@@ Property / OpenAlex ID: W1413051680 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q108482217
@@ Property / Wikidata QID: Q108482217 / rank @@
+Normal rank
@@ Property / cites work @@
+Premise selection for mathematics by corpus analysis and kernel methods
+Normal rank
@@ Property / cites work @@
+OTTER Proofs in Tarskian Geometry
@@ Property / cites work: OTTER Proofs in Tarskian Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Hammering towards QED
@@ Property / cites work: Hammering towards QED / rank @@
+Normal rank
@@ Property / cites work @@
+A Decision Algorithm for Stratified Context Unification
+Normal rank
@@ Property / cites work @@
+An application of automated reasoning in natural language question answering
+Normal rank
@@ Property / cites work @@
+Sine Qua Non for Large Theory Reasoning
@@ Property / cites work: Sine Qua Non for Large Theory Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+The 481 Ways to Split a Clause and Deal with Propositional Variables
+Normal rank
@@ Property / cites work @@
+MizAR 40 for Mizar 40
@@ Property / cites work: MizAR 40 for Mizar 40 / rank @@
+Normal rank
@@ Property / cites work @@
+Matrix interpretations for proving termination of term rewriting
+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 @@
+Lemmatization for Stronger Reasoning in Large Theories
+Normal rank
@@ Property / cites work @@
+MaSh: Machine Learning for Sledgehammer
@@ Property / cites work: MaSh: Machine Learning for Sledgehammer / rank @@
+Normal rank
@@ Property / cites work @@
+Lightweight relevance filtering for machine-generated resolution problems
+Normal rank
@@ Property / cites work @@
+Q4032144
@@ Property / cites work: Q4032144 / rank @@
+Normal rank
@@ Property / cites work @@
+System Description: E 1.8
@@ Property / cites work: System Description: E 1.8 / rank @@
+Normal rank
@@ Property / cites work @@
+The IJCAR ATP system competition
@@ Property / cites work: The IJCAR ATP system competition / 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
@@ Property / cites work @@
+Minimal and complete word unification
@@ Property / cites work: Minimal and complete word unification / rank @@
+Normal rank
@@ Property / cites work @@
+SRASS - A Semantic Relevance Axiom Selection System
+Normal rank
@@ Property / cites work @@
+MPTP-motivation, implementation, first experiments
+Normal rank
@@ Property / cites work @@
+MPTP 0.2: Design, implementation, and initial experiments
+Normal rank
@@ Property / cites work @@
+Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
+Normal rank
@@ Property / cites work @@
+AVATAR: The Architecture for First-Order Theorem Provers
+Normal rank