Crate pocket_prover [−] [src]
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: {}", prove3(&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)
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 bool
with u64
and organizing inputs
using bit patterns that simulate a truth table of 6 arguments.
To extend to 10 arguments, T
and F
are used to alternate the 4 extra arguments.
Constants
F |
The False proposition.
Used to alternate higher than 6 arguments, set to |
P0 |
0xaaaa_aaaa_aaaa_aaaa |
P1 |
0xcccc_cccc_cccc_cccc |
P2 |
0xf0f0_f0f0_f0f0_f0f0 |
P3 |
0xff00_ff00_ff00_ff00 |
P4 |
0xffff_0000_ffff_0000 |
P5 |
0xffff_ffff_0000_0000 |
T |
The True proposition.
Used to alternate higher than 6 arguments, set to |
Traits
Enumerable |
Implemented by types to use with |
Functions
all |
Enumerates the type, checking that all outputs are true. |
and |
Returns |
and3 |
And and relation of 3 argument. |
and4 |
An and relation of 4 arguments. |
and5 |
An and relation of 5 arguments. |
and6 |
An and relation of 6 arguments. |
and7 |
An and relation of 7 arguments. |
and8 |
An and relation of 8 arguments. |
and9 |
An and relation of 9 arguments. |
and10 |
An and relation of 10 arguments. |
andn |
An and relation of variable number of arguments. |
any |
Enumerates the type, checking that at least one output is true. |
count1 |
Counts the number of solutions of a 1-argument boolean function. |
count2 |
Counts the number of solutions of a 2-argument boolean function. |
count3 |
Counts the number of solutions of a 3-argument boolean function. |
count4 |
Counts the number of solutions of a 4-argument boolean function. |
count5 |
Counts the number of solutions of a 5-argument boolean function. |
count6 |
Counts the number of solutions of a 6-argument boolean function. |
count7 |
Counts the number of solutions of a 7-argument boolean function. |
count8 |
Counts the number of solutions of an 8-argument boolean function. |
count9 |
Counts the number of solutions of a 9-argument boolean function. |
count10 |
Counts the number of solutions of a 10-argument boolean function. |
countn |
Counts the number of solutions of an n-argument boolean function. |
eq |
Returns |
false_1 |
Ignores argument, always returning |
false_2 |
Ignores both arguments, returning |
false_3 |
Ignores all 3 arguments, returning |
false_4 |
Ignores all 4 arguments, returning |
false_5 |
Ignores all 5 arguments, returning |
false_6 |
Ignores all 6 arguments, returning |
false_7 |
Ignores all 7 arguments, returning |
false_8 |
Ignores all 8 arguments, returning |
false_9 |
Ignores all 9 arguments, returning |
false_10 |
Ignores all 10 arguments, returning |
id |
Returns argument. |
imply |
First argument implies the second. |
imply3 |
An imply chain of 3 arguments. |
imply4 |
An imply chain of 4 arguments. |
imply5 |
An imply chain of 5 arguments. |
imply6 |
An imply chain of 6 arguments. |
imply7 |
An imply chain of 7 arguments. |
imply8 |
An imply chain of 8 arguments. |
imply9 |
An imply chain of 9 arguments. |
imply10 |
An imply chain of 10 arguments. |
implyn |
An imply chain of variable number of arguments. |
not |
If input is |
or |
Returns |
or3 |
An or relation of 3 arguments. |
or4 |
An or relation of 4 arguments. |
or5 |
An or relation of 5 arguments. |
or6 |
An or relation of 6 arguments. |
or7 |
An or relation of 7 arguments. |
or8 |
An or relation of 8 arguments. |
or9 |
An or relation of 9 arguments. |
or10 |
An or relation of 10 arguments. |
orn |
An or relation of variable number of arguments. |
prop |
Returns |
prove1 |
Returns |
prove2 |
Returns |
prove3 |
Returns |
prove4 |
Returns |
prove5 |
Returns |
prove6 |
Returns |
prove7 |
Returns |
prove8 |
Returns |
prove9 |
Returns |
prove10 |
Returns |
proven |
Returns |
true_1 |
Ignores argument, always returning |
true_2 |
Ignores both arguments, returning |
true_3 |
Ignores all 3 arguments, returning |
true_4 |
Ignores all 4 arguments, returning |
true_5 |
Ignores all 5 arguments, returning |
true_6 |
Ignores all 6 arguments, returning |
true_7 |
Ignores all 7 arguments, returning |
true_8 |
Ignores all 8 arguments, returning |
true_9 |
Ignores all 9 arguments, returning |
true_10 |
Ignores all 10 arguments, returning |
xor |
Returns |
xor3 |
An xor relation of 3 arguments. |
xor4 |
An xor relation of 4 arguments. |
xor5 |
An xor relation of 5 arguments. |
xor6 |
An xor relation of 6 arguments. |
xor7 |
An xor relation of 7 arguments. |
xor8 |
An xor relation of 8 arguments. |
xor9 |
An xor relation of 9 arguments. |
xor10 |
An xor relation of 10 arguments. |
xorn |
An xor relation of variable number of arguments. |
Type Definitions
Pred1 |
A boolean function of one argument. |
Pred2 |
A boolean function (transformed) of two arguments. |