Computational logic: its origins and applications

DOI10.1098/RSPA.2017.0872MaRDI QIDQ4559535zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

theorem proving formal verification Isabelle proof assistants logic 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)

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.

Recommendations

Cites work

Cited in

(17)

Describes a project that uses

Uses Software

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)