Add more books on Logic, Coq, Prolog.
Chris Pressey
11 months ago
| 12 | 12 |
* date: 2024
|
| 13 | 13 |
* online @ [softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/)
|
| 14 | 14 |
|
| 15 | |
So this is actually a collection of several volumns. Should I split it up? Not sure.
|
|
15 |
So this is actually a collection of several volumes. Should I split it up? Not sure.
|
| 16 | 16 |
|
| 17 | 17 |
As of 2024 the first volume is at version 6.6. I don't know when this started.
|
|
18 |
|
|
19 |
### Certified Programming with Dependent Types
|
|
20 |
|
|
21 |
* subtitle: A Pragmatic Introduction to the Coq Proof Assistant
|
|
22 |
* author: Adam Chlipala
|
|
23 |
* date: 2013
|
|
24 |
* online @ [archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes)
|
|
25 |
|
|
26 |
I haven't read it, but this is an open-access book about Coq.
|
| 35 | 35 |
### Books
|
| 36 | 36 |
|
| 37 | 37 |
Software Foundations (online @ [softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/))
|
|
38 |
|
|
39 |
Certified Programming with Dependent Types (online @ [archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes))
|
| 8 | 8 |
|
| 9 | 9 |
### Introduction to Combinators and the Lambda Calculus
|
| 10 | 10 |
|
| 11 | |
* author: J. Roger Hindley, Jonathon P. Seldin
|
|
11 |
* author: J. Roger Hindley, Jonathan P. Seldin
|
| 12 | 12 |
* date: 1986
|
| 13 | 13 |
* borrow @ [archive.org](https://archive.org/details/introductiontoco0000hind)
|
| 14 | 14 |
|
| 16 | 16 |
A fairly gentle introduction to formal logic, starting with propositional logic,
|
| 17 | 17 |
then first-order, first-order with equality, second-order logic, then the
|
| 18 | 18 |
Peano axioms, and so on.
|
|
19 |
|
|
20 |
### Mathematical Logic
|
|
21 |
|
|
22 |
* author: Stephen Cole Kleene
|
|
23 |
* date: 1967
|
|
24 |
* borrow @ [archive.org](https://archive.org/details/mathematicallogi0000klee)
|
|
25 |
* other-topics: FoM, Computability
|
|
26 |
|
|
27 |
A book on mathematical logic written by Kleene.
|
|
28 |
|
|
29 |
### Deductive Logic: a programed introduction
|
|
30 |
|
|
31 |
* author: John T. Kearns
|
|
32 |
* date: 1969
|
|
33 |
* borrow @ [archive.org](https://archive.org/details/deductivelogicpr0000john)
|
|
34 |
|
|
35 |
"Programed" means the thing is one big exercise sheet. Individual questions with
|
|
36 |
answers are called "frames". In fact, "The Little Lisper", "The Little Schemer",
|
|
37 |
"The Reasoned Schemer", etc, are all in this format too.
|
| 35 | 35 |
### Books
|
| 36 | 36 |
|
| 37 | 37 |
Mathematical logic and formalized theories (borrow @ [archive.org](https://archive.org/details/mathematicallogi0000roge))
|
|
38 |
|
|
39 |
Mathematical Logic (borrow @ [archive.org](https://archive.org/details/mathematicallogi0000klee))
|
|
40 |
|
|
41 |
Deductive Logic: a programed introduction (borrow @ [archive.org](https://archive.org/details/deductivelogicpr0000john))
|
|
0 |
Prolog Books
|
|
1 |
============
|
|
2 |
|
|
3 |
<!--
|
|
4 |
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
|
|
5 |
|
|
6 |
SPDX-License-Identifier: CC0-1.0
|
|
7 |
-->
|
|
8 |
|
|
9 |
### Programming in PROLOG
|
|
10 |
|
|
11 |
* author: Clocksin and Mellish
|
|
12 |
* date: 1985
|
|
13 |
* borrow @ [archive.org](https://archive.org/details/programminginpro00cloc)
|
|
14 |
|
|
15 |
Sort of a classic.
|
|
16 |
|
|
17 |
### The Art of Prolog
|
|
18 |
|
|
19 |
* author: Leon Sterling
|
|
20 |
* date: 1994
|
|
21 |
* borrow @ [archive.org](https://archive.org/details/artofprologadvan0000ster)
|
|
22 |
|
|
23 |
A good book about Prolog programming.
|
| 25 | 25 |
[search - Prolog: Element not present in list - Stack Overflow](https://stackoverflow.com/questions/5872790/prolog-element-not-present-in-list)
|
| 26 | 26 |
|
| 27 | 27 |
[Index of /nofib/real/prolog/](http://darcs.haskell.org/nofib/real/prolog/)
|
|
28 |
|
|
29 |
### Books
|
|
30 |
|
|
31 |
Programming in PROLOG (borrow @ [archive.org](https://archive.org/details/programminginpro00cloc))
|
|
32 |
|
|
33 |
The Art of Prolog (borrow @ [archive.org](https://archive.org/details/artofprologadvan0000ster))
|
|
0 |
Prolog
|
|
1 |
------
|
|
2 |
|
|
3 |
<!--
|
|
4 |
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
|
|
5 |
|
|
6 |
SPDX-License-Identifier: CC0-1.0
|
|
7 |
-->
|
|
8 |
|
|
9 |
- - - -
|
|
10 |
|
|
11 |
[SWI-Prolog \-- Manual](https://www.swi-prolog.org/pldoc/man?section=preddesc)
|
|
12 |
|
|
13 |
[Prolog Tutorial \-- 2.5 (wayback)](https://web.archive.org/web/20120203025542/http://www.csupomona.edu/~jrfisher/www/prolog_tutorial/2_5.html)
|
|
14 |
|
|
15 |
[Prolog Guide - Data Structures](http://kti.ms.mff.cuni.cz/~bartak/prolog/data_struct.html)
|
|
16 |
|
|
17 |
[Parsing in Prolog](https://www2.cs.sfu.ca/~cameron/Teaching/383/DCG.html)
|
|
18 |
|
|
19 |
[A Couple of Meta-interpreters in Prolog](https://www.metalevel.at/acomip/)
|
|
20 |
|
|
21 |
[What does \\+ mean in Prolog? - Stack Overflow](https://stackoverflow.com/questions/1712034/what-does-mean-in-prolog)
|
|
22 |
|
|
23 |
[search - Prolog: Element not present in list - Stack Overflow](https://stackoverflow.com/questions/5872790/prolog-element-not-present-in-list)
|
|
24 |
|
|
25 |
[Index of /nofib/real/prolog/](http://darcs.haskell.org/nofib/real/prolog/)
|