Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
Review
. 2018 Feb;474(2210):20170872.
doi: 10.1098/rspa.2017.0872. Epub 2018 Feb 28.

Computational logic: its origins and applications

Lawrence C Paulson  1
Affiliations
Review

Computational logic: its origins and applications

Lawrence C Paulson. Proc Math Phys Eng Sci. 2018 Feb.

Abstract

Computational logic is the use of computers to establish facts in a logical formalism. Originating in nineteenth 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 'logic for computable functions (LCF) approach' pioneered by Robin Milner, 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.

Keywords: Isabelle; formal verification; logic for computable functions; proof assistants; theorem proving.

PubMed Disclaimer

Conflict of interest statement

I declare I have no competing interest.

Similar articles

See all similar articles

Cited by

References

    1. Woollaston V. 2017. WannaCry ransomware: what is it and how to protect yourself. See http://www.wired.co.uk/article/wannacry-ransomware-virus-patch.
    1. Nicely TR. 2011. Pentium FDIV flaw. See http://www.trnicely.net/pentbug/pentbug.html.
    1. Lowe G. 1996. Some new attacks upon security protocols. In Proc. 9th Computer Security Foundations Workshop, pp. 162–169. Silver Spring, MD: IEEE Computer Society Press.
    1. Boolos GS. 1998. Gottlob Frege and the foundations of arithmetic. In Logic, logic, and logic (ed. GS Boolos), pp. 143–154. Cambridge, MA: Harvard University Press.
    1. Gödel K. 1983. Russell’s mathematical logic. In Philosophy of mathematics: selected readings (eds P Benacerraf, H Putnam), 2nd edn, pp. 447–469. Cambridge, UK: Cambridge University Press.

LinkOut - more resources