Repository logo
 

Computational logic: its origins and applications.

Accepted version
Peer-reviewed

Type

Article

Change log

Authors

Paulson, Lawrence C  ORCID logo  https://orcid.org/0000-0003-0288-4279

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.

Description

Keywords

Isabelle, formal verification, logic for computable functions, proof assistants, theorem proving

Journal Title

Proc Math Phys Eng Sci

Conference Name

Journal ISSN

1364-5021
1471-2946

Volume Title

474

Publisher

The Royal Society