theoremprover-museum / theoremprover-museum.github.io

https://theoremprover-museum.github.io
GNU General Public License v3.0
52 stars 7 forks source link

Autologic --> Most Wanted Prover Museum #24

Open ghost opened 3 years ago

ghost commented 3 years ago

Dear Prof Kohlhase,

How about adding Autologic from Neil Tennant? https://theoremprover-museum.github.io/wanted/

I find:

Autologic Shows how to program on a computer (in Prolog) the effective skills taught in introductory and intermediate logic courses. The topics include the relevance of relevance, representing formulae and proofs, avoiding loops and blind alleys, and other aspects. Of interest to computational logicians, proof-theorists, cognitive scientists, and workers in artificial intelligence. Distributed by Columbia U. Press. Annotation copyright by Book News, Inc., Portland, OR https://www.amazon.de/dp/0748603581

And here some usage:

There was at least person who even read the book: % and I learnt a trick or two from Neil Tennant's "Autologic" book. https://github.com/ptarau/TypesAndProofs/blob/master/third_party/dyckhoff_orig.pro

It could be that Autologic was heading towards Logic of Paradox from Graham Priest, but I am currently not yet sure whats the content of Autologic, since I could not yet grab a copy, neither some code snippets from it.

Best Regards