pocket_prover

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

For generic automated theorem proving, see monotonic_solver.

```rust extern crate pocket_prover;

use pocket_prover::*;

fn main() { println!("Socrates is mortal: {}", prove3(|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.