First-Order Logic According to Harrison

Alexander Birch Jensen; Anders Schlichtkrull; Jørgen Villadsen

First-Order Logic According to Harrison

Alexander Birch Jensen
, Anders Schlichtkrull
, Jørgen Villadsen

Department of Applied Mathematics and Computer Science

Research output: Contribution to journal › Journal article › Research › peer-review

331 Downloads (Orbit)

Abstract

We present a certified declarative first-order prover with equality based on John Harrison’s Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009. ML code reflection is used such that the entire prover can be executed within Isabelle as a very simple interactive proof assistant. As examples we consider Pelletier’s problems 1-46.

Original language	English
Book series	Archive of Formal Proofs
Pages (from-to)	1-66
ISSN	2150-914X
Publication status	Published - 2017

Access to Document

DocumentFinal published version, 225 KB

https://www.isa-afp.org/entries/FOL_Harrison.shtml

OpenUrl availability

Full text

Cite this

@article{f6c14f31cace4f0f8ef3b7e0de656082,

title = "First-Order Logic According to Harrison",

abstract = "We present a certified declarative first-order prover with equality based on John Harrison{\textquoteright}s Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009. ML code reflection is used such that the entire prover can be executed within Isabelle as a very simple interactive proof assistant. As examples we consider Pelletier{\textquoteright}s problems 1-46.",

author = "Jensen, \{Alexander Birch\} and Anders Schlichtkrull and J{\o}rgen Villadsen",

year = "2017",

language = "English",

pages = "1--66",

journal = "Archive of Formal Proofs",

issn = "2150-914X",

publisher = "SourceForge",

}

TY - JOUR

T1 - First-Order Logic According to Harrison

AU - Jensen, Alexander Birch

AU - Schlichtkrull, Anders

AU - Villadsen, Jørgen

PY - 2017

Y1 - 2017

N2 - We present a certified declarative first-order prover with equality based on John Harrison’s Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009. ML code reflection is used such that the entire prover can be executed within Isabelle as a very simple interactive proof assistant. As examples we consider Pelletier’s problems 1-46.

AB - We present a certified declarative first-order prover with equality based on John Harrison’s Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009. ML code reflection is used such that the entire prover can be executed within Isabelle as a very simple interactive proof assistant. As examples we consider Pelletier’s problems 1-46.

M3 - Journal article

SN - 2150-914X

SP - 1

EP - 66

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

ER -

First-Order Logic According to Harrison

Abstract

Access to Document

OpenUrl availability

Fingerprint

Cite this