Automating free logic in HOL, with an experimental application in category theory (Q2303232): Difference between revisions

@@ Property / DOI @@
-.1007/s10817-018-09507-7
@@ Property / DOI: 10.1007/s10817-018-09507-7 / 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 @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / 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 @@
+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 @@
+CVC4
@@ Property / describes a project that uses: CVC4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Leo-III
@@ Property / describes a project that uses: Leo-III / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2908410917
@@ Property / OpenAlex ID: W2908410917 / rank @@
+Normal rank
@@ Property / cites work @@
+General models and extensionality
@@ Property / cites work: General models and extensionality / rank @@
+Normal rank
@@ Property / cites work @@
+Q3077958
@@ Property / cites work: Q3077958 / rank @@
+Normal rank
@@ Property / cites work @@
+Cut-elimination for quantified conditional logic
@@ Property / cites work: Cut-elimination for quantified conditional logic / rank @@
+Normal rank
@@ Property / cites work @@
+Higher-order semantics and extensionality
@@ Property / cites work: Higher-order semantics and extensionality / rank @@
+Normal rank
@@ Property / cites work @@
+Cut-Simulation and Impredicativity
@@ Property / cites work: Cut-Simulation and Impredicativity / rank @@
+Normal rank
@@ Property / cites work @@
+Computational logic
@@ Property / cites work: Computational logic / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Free Logic in Isabelle/HOL
@@ Property / cites work: Automating Free Logic in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+The higher-order prover \textsc{Leo}-II
@@ Property / cites work: The higher-order prover \textsc{Leo}-II / rank @@
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT solvers
@@ Property / cites work: Extending Sledgehammer with SMT solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
+Normal rank
@@ Property / cites work @@
+More SPASS with Isabelle
@@ Property / cites work: More SPASS with Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Satallax: An Automatic Higher-Order Prover
@@ Property / cites work: Satallax: An Automatic Higher-Order Prover / rank @@
+Normal rank
@@ Property / cites work @@
+A formulation of the simple theory of types
@@ Property / cites work: A formulation of the simple theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+Q3995720
@@ Property / cites work: Q3995720 / rank @@
+Normal rank
@@ Property / cites work @@
+Groups, Categories and Duality
@@ Property / cites work: Groups, Categories and Duality / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings
+Normal rank
@@ Property / cites work @@
+Q3208629
@@ Property / cites work: Q3208629 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3075241
@@ Property / cites work: Q3075241 / rank @@
+Normal rank
@@ Property / DOI @@
+.1007/S10817-018-09507-7
@@ Property / DOI: 10.1007/S10817-018-09507-7 / rank @@
+Normal rank