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 `0`.
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 `1`.

Traits

Enumerable

Implemented by types to use with all and any.

Functions

all	Enumerates the type, checking that all outputs are true.
and	Returns `true` if all arguments are `true`.
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 `true` if arguments are equal.
false_1	Ignores argument, always returning `false`.
false_2	Ignores both arguments, returning `false` for all inputs.
false_3	Ignores all 3 arguments, returning `false` for all inputs.
false_4	Ignores all 4 arguments, returning `false` for all inputs.
false_5	Ignores all 5 arguments, returning `false` for all inputs.
false_6	Ignores all 6 arguments, returning `false` for all inputs.
false_7	Ignores all 7 arguments, returning `false` for all inputs.
false_8	Ignores all 8 arguments, returning `false` for all inputs.
false_9	Ignores all 9 arguments, returning `false` for all inputs.
false_10	Ignores all 10 arguments, returning `false` for all inputs.
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 `true`, returns `false` and vice versa.
or	Returns `true` if at least one argument is `true`.
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 `T` if `a` is `true`, `F` otherwise. In logical terminology this corresponds to a proposition.
prove1	Returns `true` if proposition is correct, `false` otherwise.
prove2	Returns `true` if proposition is correct, `false` otherwise.
prove3	Returns `true` if proposition is correct, `false` otherwise.
prove4	Returns `true` if proposition is correct, `false` otherwise.
prove5	Returns `true` if proposition is correct, `false` otherwise.
prove6	Returns `true` if proposition is correct, `false` otherwise.
prove7	Returns `true` if proposition is correct, `false` otherwise.
prove8	Returns `true` if proposition is correct, `false` otherwise.
prove9	Returns `true` if proposition is correct, `false` otherwise.
prove10	Returns `true` if proposition is correct, `false` otherwise.
proven	Returns `true` if proposition is correct, `false` otherwise.
true_1	Ignores argument, always returning `true`.
true_2	Ignores both arguments, returning `true` for all inputs.
true_3	Ignores all 3 arguments, returning `true` for all inputs.
true_4	Ignores all 4 arguments, returning `true` for all inputs.
true_5	Ignores all 5 arguments, returning `true` for all inputs.
true_6	Ignores all 6 arguments, returning `true` for all inputs.
true_7	Ignores all 7 arguments, returning `true` for all inputs.
true_8	Ignores all 8 arguments, returning `true` for all inputs.
true_9	Ignores all 9 arguments, returning `true` for all inputs.
true_10	Ignores all 10 arguments, returning `true` for all inputs.
xor	Returns `true` if only one argument is `true`.
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.