Computational logic: its origins and applications

DOI10.1098/RSPA.2017.0872zbMATH Open1402.68160arXiv1712.04375OpenAlexW3099800985WikidataQ55174437 ScholiaQ55174437MaRDI QIDQ4559535FDOQ4559535

Authors: Lawrence C. Paulson 

Publication date: 4 December 2018

Published in: Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences (Search for Journal in Brave)

Abstract: Computational Logic is the use of computers to establish facts in a logical formalism. Originating in 19th-century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the "LCF approach" pioneered by Robin Milner FRS, where proofs can be constructed interactively or with the help of users' code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.

Full work available at URL: https://arxiv.org/abs/1712.04375

Recommendations

• Computational logic and set theory. Applying formalized logic to analysis. Foreword by Martin Davis
• scientific article; zbMATH DE number 5194318
• Logic and Computation
• Towards a mechanically checked theory of computation. The ACL2 project
• Logics, mathematics, automatic deduction

zbMATH Keywords

theorem provingformal verificationIsabelleproof assistantslogic for computable functions

Mathematics Subject Classification ID

History of mathematics in the 20th century (01A60) History of computer science (68-03) Specification and verification (program logics, model checking, etc.) (68Q60) History of mathematics in the 21st century (01A61) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• Edinburgh LCF. A mechanized logic of computation
• Coquelicot: a user-friendly library of real analysis for Coq
• Flyspeck I: Tame Graphs
• Set theory. An introduction to independence proofs
• A framework for defining logics
• Title not available (Why is that?)
• Logic in Computer Science
• Title not available (Why is that?)
• Title not available (Why is that?)
• Homotopy type theory. Univalent foundations of mathematics
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Solution of the Robbins problem
• A formally verified proof of the central limit theorem
• A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
• Title not available (Why is that?)
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• CakeML
• Commutative algebra in the Mizar system
• The calculus of constructions
• Software model checking
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Title not available (Why is that?)
• The Jordan Curve Theorem, Formally and Informally
• The Four Colour Theorem: Engineering of a Formal Proof
• A machine-checked proof of the odd order theorem
• Title not available (Why is that?)
• Verification of the Miller-Rabin probabilistic primality test.
• Title not available (Why is that?)
• Natural deduction as higher-order resolution
• A revision of the proof of the Kepler conjecture
• The foundation of a generic theorem prover
• Constructive mathematics and computer programming
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Title not available (Why is that?)
• Proof assistants: history, ideas and future
• Title not available (Why is that?)
• Formal verification of a floating-point expansion renormalization algorithm
• Markov chains and Markov decision processes in Isabelle/HOL
• Formalizing an analytic proof of the prime number theorem
• A term of length 4 523 659 424 929
• Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
• Formalization of the fundamental group in untyped set theory using auto2

Cited In (17)

• Reasoning, Logic and Computation
• Computational Logic and Continuous Mathematics, Pure and Applied
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formalising Mathematics in Simple Type Theory
• Logics, mathematics, automatic deduction
• 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
• Title not available (Why is that?)
• Logic and Computation
• On the unusual effectiveness of logic in computer science
• Formalising basic topology for computational logic in simple type theory
• From LCF to Isabelle/HOL
• Title not available (Why is that?)
• Connecting logical representations and efficient computations
• Title not available (Why is that?)
• Computer Science Logic

Uses Software

• Coq
• Isabelle
• Nitpick
• ML
• Mizar
• HOL
• HOL Light
• Sledgehammer
• Automath
• CakeML
• Flyspeck
• Coquelicot
• seL4
• Jordan
• kepler98
• Tame Graphs

This page was built for publication: Computational logic: its origins and applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4559535)