| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
First-Order Logic According to Harrison
| Title: | First-Order Logic According to Harrison |
| Authors: | Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen |
| Submission date: | 2017-01-01 |
| 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. |
| BibTeX: |
@article{FOL_Harrison-AFP,
author = {Alexander Birch Jensen and Anders Schlichtkrull and Jørgen Villadsen},
title = {First-Order Logic According to Harrison},
journal = {Archive of Formal Proofs},
month = jan,
year = 2017,
note = {\url{http://isa-afp.org/entries/FOL_Harrison.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
| Older releases: None |