Computational logic: its origins and applications
From MaRDI portal
Publication:4559535
DOI10.1098/rspa.2017.0872zbMath1402.68160arXiv1712.04375OpenAlexW3099800985WikidataQ55174437 ScholiaQ55174437MaRDI QIDQ4559535
Publication date: 4 December 2018
Published in: Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1712.04375
History of mathematics in the 20th century (01A60) History of mathematics in the 21st century (01A61) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) History of computer science (68-03)
Related Items
A modular first formalisation of combinatorial design theory, Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started, Formalising Mathematics in Simple Type Theory, Formalising basic topology for computational logic in simple type theory, From LCF to Isabelle/HOL
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Commutative algebra in the Mizar system
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A revision of the proof of the Kepler conjecture
- Proof assistants: history, ideas and future
- The calculus of constructions
- Set theory. An introduction to independence proofs
- Solution of the Robbins problem
- Verification of the Miller-Rabin probabilistic primality test.
- Formal verification of a floating-point expansion renormalization algorithm
- A formally verified proof of the central limit theorem
- Markov chains and Markov decision processes in Isabelle/HOL
- Edinburgh LCF. A mechanized logic of computation
- The foundation of a generic theorem prover
- A term of length 4 523 659 424 929
- Coquelicot: a user-friendly library of real analysis for Coq
- Formalizing an analytic proof of the prime number theorem
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
- Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
- Constructive mathematics and computer programming
- The Four Colour Theorem: Engineering of a Formal Proof
- Flyspeck I: Tame Graphs
- A framework for defining logics
- Natural deduction as higher-order resolution
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- Logic in Computer Science
- Software model checking
- A Machine-Checked Proof of the Odd Order Theorem
- Formal certification of a compiler back-end or
- CakeML
- Homotopy Type Theory: Univalent Foundations of Mathematics
- The Jordan Curve Theorem, Formally and Informally
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Formalization of the fundamental group in untyped set theory using auto2
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
