## Tree @develop-202209xx (Download .tar.gz)

# Philomath

*See also:* LCF-style-ND
∘ Maxixe
∘ Cardboard Prolog

**Philomath** is an LCF-style theorem prover written in ANSI C. It implements
classical propositional logic inside a Natural Deduction system with
labelled assumptions. For more information on this approach, see the
**LCF-style-ND** repository.

## How do I write a proof with this?

Create a file `myproof.c`

:

```
#include "formula.h"
#include "proof.h"
int main(int argc, char **argv) {
/* Proof of p -> p */
return proves(
impl_intro(1, suppose(var("p"), 1)),
impl(var("p"), var("p"))
);
}
```

Then compile and run it with:

```
./build-proof.sh myproof
```

And run the resulting executable:

```
./myproof.exe
```

If the exit code is 0, the proof is valid!

```
% echo $?
0
```

If you wish to build the proof with debugging output, you can pass the `-D`

flag:

```
./build-proof.sh -D myproof
```

## Limitations

LCF-style theorem proving relies on data abstraction, i.e. information hiding.
In C, information hiding is accomplished by exposing, in a header file, only the
fact that a `struct`

exists, and *not* exposing its structure. Client code can then
work with pointers to that `struct`

without knowing what's contained in it.

It is however possible to subvert this mechanism. If your proof code does any of the following things, it is possible it is no longer a valid proof:

- includes the file
`proof.c`

directly, rather than including`proof.h`

- casts a
`struct theorem`

value to some other type - casts a value of some other type to a
`struct theorem`

Fortunately, it is possible to statically analyze a C source file and confirm that it does none of these things, if such a level of assurance is desired.

## TODO

Should really have more demo non-proofs, to check that it's not letting non-proofs pass themselves off as proofs.

Could stand to have a real suite of unit tests instead of just a handful of demo proofs than you can build and run manually.

##
Commit History
@develop-202209xx
`git clone https://git.catseye.tc/Philomath/`

- Rename from "proof.c" to "theorem.c" because it defines theorems. Chris Pressey 1 year, 10 months ago
- Fix typo in comment. Chris Pressey 1 year, 10 months ago
- "struct theorem" is a better name than "struct proof" for this. Chris Pressey 1 year, 10 months ago
- Add "see-also bar" to top of README. Chris Pressey 2 years ago
- Add UNLICENSE. Chris Pressey 2 years ago
- "Progress" is done, replace with a "To do" section. Chris Pressey 2 years ago
- Use less confusing (maybe) parameter names x, y, z for input proofs. Chris Pressey 2 years ago
- Implement double_neg_elim. Demo proof of reductio ad absurdum. Chris Pressey 2 years ago
- Implement neg_intro(). Chris Pressey 2 years ago
- Finish the proof by simulating the copy rule with conj-intro-elim. Chris Pressey 2 years ago