Actions

Computational Logic

Revision as of 23:12, 24 March 2021 by User (talk | contribs) (Created page with "'''Computational Logic''' is the use of logic to perform or reason about computation. It bears a similar relationship to computer science and engineering as mathematical logic...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Computational Logic is the use of logic to perform or reason about computation. It bears a similar relationship to computer science and engineering as mathematical logic bears to mathematics and as philosophical logic bears to philosophy. It is synonymous with "logic in computer science.[1]

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.[2]

  1. Definition - What Does Computational Logic Mean? Wikipedia
  2. Explaining Computational Logic The Royal Society