First-Order Logic According to Harrison

Research output: Contribution to journalJournal articleResearchpeer-review

181 Downloads (Pure)

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 languageEnglish
Book seriesArchive of Formal Proofs
Pages (from-to)1-66
ISSN2150-914X
Publication statusPublished - 2017

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’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.",
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",

}

First-Order Logic According to Harrison. / Jensen, Alexander Birch; Schlichtkrull, Anders; Villadsen, Jørgen.

In: Archive of Formal Proofs, 2017, p. 1-66.

Research output: Contribution to journalJournal articleResearchpeer-review

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

SP - 1

EP - 66

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

SN - 2150-914X

ER -