FOL_Harrison (Q43931)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry FOL_Harrison
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | FOL_Harrison |
AFP entry FOL_Harrison |
Statements
Alexander Birch Jensen
0 references
Anders Schlichtkrull
0 references
Jørgen Villadsen
0 references
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. Reference: Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL. Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen. AI Communications 31:281-299 2018. https://content.iospress.com/articles/ai-communications/aic764 See also: Students' Proof Assistant (SPA). https://github.com/logic-tools/spa
0 references
1 January 2017
0 references
First-Order Logic According to Harrison (English)
0 references
