### 26 releases (15 breaking)

0.17.0 | Oct 7, 2022 |
---|---|

0.16.0 | Jun 20, 2022 |

0.15.0 | May 13, 2022 |

0.13.2 | Mar 30, 2022 |

0.1.0 | Nov 5, 2017 |

#**99** in Math

**76** downloads per month

Used in **2** crates

**MIT**license

99KB

1.5K
SLoC

# Pocket-Prover

A fast, brute force, automatic theorem prover for first order logic

- For generic automated theorem proving, see monotonic_solver
- For a debuggable SAT solver, see debug_sat

`extern` `crate` pocket_prover`;`
`use` `pocket_prover``::``*``;`
`fn` `main``(``)`` ``{`
`println!``(``"`Socrates is mortal: `{}``"``,` `prove!``(``&``mut` `|`man`,` mortal`,` socrates`|` `{`
`//` Using `imply` because we want to prove an inference rule.
`imply``(`
`//` Premises.
`and``(`
`//` All men are mortal.
`imply``(`man`,` mortal`)``,`
`//` Socrates is a man.
`imply``(`socrates`,` man`)``,`
`)``,`
`//` Conclusion.
`imply``(`socrates`,` mortal`)`
`)`
`}``)``)``;`
`}`

### Motivation

The motivation is to provide the analogue of a "pocket calculator", but for logic, therefore called a "pocket prover".

This library uses an approach that is simple to implement from scratch in a low level language.

This is useful in cases like:

- Study logic without the hurdle of doing manual proofs
- Checking your understanding of logic
- Verify that logicians are wizards and not lizards
- Due to a series of unfortunate events, you got only 24 hours to learn logic and just need the gist of it
- Memorizing source code for situations like The Martian
- A tiny mistake and the whole planet blows up (e.g. final decisions before the AI singularity and you need to press the right buttons)

In addition this library can be used to create extensible logical systems.
For more information, see the

trait.`Prove`

### Implementation

This library uses brute-force to check proofs, instead of relying on axioms of logic.

64bit CPUs are capable of checking logical proofs of 6 arguments (booleans)
in O(1), because proofs can be interpreted as tautologies (true for all input)
and

.`2``^``6` `=` `64`

This is done by replacing

with `bool`

and organizing inputs
using bit patterns that simulate a truth table of 6 arguments.`u64`

To extend to 10 arguments,

and `T`

are used to alternate the 4 extra arguments.
To extend to N arguments, recursive calls are used down to less than 10 arguments.`F`

### Path Semantical Logic

*Notice! Path Semantical Logic is at early stage of research.*

This library has experimental support for a subset of Path Semantical Logic. Implementation is based on paper Faster Brute Force Proofs.

Path Semantical Logic separates propositions into levels, such that an equality between two propositions in level N+1, propagates into equality between uniquely associated propositions in level N.

For example, if

has level 1 and `f`

has level 0,
then `x`

associates `imply``(`f`,` x`)`

uniquely with `x`

,
such that the core axiom of Path Semantics
is satisfied.`f`

This library has currently only support for level 1 and 0.
These functions are prefixed with

.`path1_`

The macros

and `count!`

will automatically expand
to `prove!`

and `path1_count !`

`path1_prove``!`

.Each function takes two arguments, consisting of tuples of propositions, e.g.

.
Arbitrary number of arguments is supported.`(`f`,` g`)``,` `(`x`,` y`)`

`extern` `crate` pocket_prover`;`
`use` `pocket_prover``::``*``;`
`fn` `main``(``)`` ``{`
`println!``(``"`=== Path Semantical Logic ===`"``)``;`
`println!``(``"`The notation `f(x)` means `x` is uniquely associated with `f`.`"``)``;`
`println!``(``"`For more information, see the section 'Path Semantical Logic' in documentation.`"``)``;`
`println!``(``"``"``)``;`
`print!``(``"`(f(x), g(y), h(z), f=g ⊻ f=h) => (x=y ∨ x=z): `"``)``;`
`println!``(``"``{}``\n``"``,` `prove!``(``&``mut` `|``(`f`,` g`,` h`)``,` `(`x`,` y`,` z`)``|` `{`
`imply``(`
`and!``(`
`imply``(`f`,` x`)``,`
`imply``(`g`,` y`)``,`
`imply``(`h`,` z`)``,`
`xor``(``eq``(`f`,` g`)``,` `eq``(`f`,` h`)``)`
`)``,`
`or``(``eq``(`x`,` y`)``,` `eq``(`x`,` z`)``)`
`)`
`}``)``)``;`
`print!``(``"`(f(x), g(y), f=g => h, h(z)) => (x=y => z): `"``)``;`
`println!``(``"``{}``\n``"``,` `prove!``(``&``mut` `|``(`f`,` g`,` h`)``,` `(`x`,` y`,` z`)``|` `{`
`imply``(`
`and!``(`
`imply``(`f`,` x`)``,`
`imply``(`g`,` y`)``,`
`imply``(``eq``(`f`,` g`)``,` h`)``,`
`imply``(`h`,` z`)`
`)``,`
`imply``(``eq``(`x`,` y`)``,` z`)`
`)`
`}``)``)``;`
`}`

### Path Semantical Quality

Pocket-Prover has a model of Path Semantical Quality that resembles quantum logic.

To write

you use `x ~~ y`

`q``(`x`,` y`)`

or `qual``(`x`,` y`)`

.

is the same as `q``(`x`,` y`)`

.
`and!``(``eq``(`x`,` y`)``,` `qubit``(`x`)``,` `qubit``(`y`)``)`

is the same as `q``(`x`,` x`)`

.`qubit``(`x`)`

A qubit is a kind of "superposition".
One can also think about it as introducing a new argument

that depends on `qubit``(`x`)`

.`x`

Since qubits can collide with other propositions,
one must repeat measurements e.g. using

to get classical states.
However, sometimes one might wish to amplify quantum states, using `measure`

or `amplify`

.`amp`

To use quality with path semantics, one should use

.
Path Semantical Logic is designed for equality, not quality.`ps_core`

`use` `pocket_prover``::``*``;`
`fn` `main``(``)`` ``{`
`println!``(``"`Path semantics: `{}``"``,` `measure``(``1``,` `|``|` `prove!``(``&``mut` `|`a`,` b`,` c`,` d`|` `{`
`imply``(`
`and!``(`
`ps_core``(`a`,` b`,` c`,` d`)``,`
`imply``(`a`,` c`)``,`
`imply``(`b`,` d`)`
`)``,`
`imply``(``qual``(`a`,` b`)``,` `qual``(`c`,` d`)``)`
`)`
`}``)``)``)``;`
`}`

#### Dependencies

~455KB