Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: First-Order Logic According t...

Email Gateway (Aug 22 2022 at 14:58):

From: Tobias Nipkow <nipkow@in.tum.de>
First-Order Logic According to Harrison

Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen

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.

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

First submission in 2017 - Happy New Year!
smime.p7s

Last updated: Apr 26 2024 at 16:20 UTC