Computational logic: its origins and applications (Q4559535): Difference between revisions

@@ Property / describes a project that uses @@
+Tame Graphs
@@ Property / describes a project that uses: Tame Graphs / 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 @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CakeML
@@ Property / describes a project that uses: CakeML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+kepler98
@@ Property / describes a project that uses: kepler98 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / 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 @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / 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 / OpenAlex ID @@
+W3099800985
@@ Property / OpenAlex ID: W3099800985 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q55174437
@@ Property / Wikidata QID: Q55174437 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.04375
@@ Property / arXiv ID: 1712.04375 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4523465
@@ Property / cites work: Q4523465 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3340832
@@ Property / cites work: Q3340832 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4523457
@@ Property / cites work: Q4523457 / rank @@
+Normal rank
@@ Property / cites work @@
+Set theory. An introduction to independence proofs
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive mathematics and computer programming
@@ Property / cites work: Constructive mathematics and computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Logic in Computer Science
@@ Property / cites work: Logic in Computer Science / rank @@
+Normal rank
@@ Property / cites work @@
+Software model checking
@@ Property / cites work: Software model checking / rank @@
+Normal rank
@@ Property / cites work @@
+A term of length 4 523 659 424 929
@@ Property / cites work: A term of length 4 523 659 424 929 / rank @@
+Normal rank
@@ Property / cites work @@
+Solution of the Robbins problem
@@ Property / cites work: Solution of the Robbins problem / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3753927
@@ Property / cites work: Q3753927 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Formal certification of a compiler back-end or
@@ Property / cites work: Formal certification of a compiler back-end or / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
+Normal rank
@@ Property / cites work @@
+Natural deduction as higher-order resolution
@@ Property / cites work: Natural deduction as higher-order resolution / rank @@
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Q3922646
@@ Property / cites work: Q3922646 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4520767
@@ Property / cites work: Q4520767 / rank @@
+Normal rank
@@ Property / cites work @@
+A formally verified proof of the central limit theorem
+Normal rank
@@ Property / cites work @@
+A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
+Normal rank
@@ Property / cites work @@
+The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
+Normal rank
@@ Property / cites work @@
+Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
+Normal rank
@@ Property / cites work @@
+Q4122841
@@ Property / cites work: Q4122841 / rank @@
+Normal rank
@@ Property / cites work @@
+Commutative algebra in the Mizar system
@@ Property / cites work: Commutative algebra in the Mizar system / rank @@
+Normal rank
@@ Property / cites work @@
+Verification of the Miller-Rabin probabilistic primality test.
+Normal rank
@@ Property / cites work @@
+Markov chains and Markov decision processes in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Formal verification of a floating-point expansion renormalization algorithm
+Normal rank
@@ Property / cites work @@
+Formalizing an analytic proof of the prime number theorem
+Normal rank
@@ Property / cites work @@
+A revision of the proof of the Kepler conjecture
@@ Property / cites work: A revision of the proof of the Kepler conjecture / rank @@
+Normal rank
@@ Property / cites work @@
+Flyspeck I: Tame Graphs
@@ Property / cites work: Flyspeck I: Tame Graphs / rank @@
+Normal rank
@@ Property / cites work @@
+The Four Colour Theorem: Engineering of a Formal Proof
+Normal rank
@@ Property / cites work @@
+Q2739733
@@ Property / cites work: Q2739733 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099559
@@ Property / cites work: Q4099559 / rank @@
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ Property / cites work @@
+Mechanizing set theory. Cardinal arithmetic and the axiom of choice
+Normal rank
@@ Property / cites work @@
+Formalization of the fundamental group in untyped set theory using auto2
+Normal rank
@@ Property / cites work @@
+Q4523464
@@ Property / cites work: Q4523464 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5639839
@@ Property / cites work: Q5639839 / rank @@
+Normal rank
@@ Property / cites work @@
+The Jordan Curve Theorem, Formally and Informally
@@ Property / cites work: The Jordan Curve Theorem, Formally and Informally / rank @@
+Normal rank
@@ Property / cites work @@
+Coquelicot: a user-friendly library of real analysis for Coq
+Normal rank
@@ Property / cites work @@
+CakeML
@@ Property / cites work: CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+Proof assistants: history, ideas and future
@@ Property / cites work: Proof assistants: history, ideas and future / rank @@
+Normal rank
@@ Property / cites work @@
+Q4619818
@@ Property / cites work: Q4619818 / rank @@
+Normal rank