# pocket_prover

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

```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 `Prove` trait.

### 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. To extend to N arguments, recursive calls are used down to less than 10 arguments.

### 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 `f` has level 1 and `x` has level 0, then `imply(f, x)` associates `x` uniquely with `f`, such that the core axiom of Path Semantics is satisfied.

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

The macros `count!` and `prove!` will automatically expand to `path1_count!` and `path1_prove!`.

Each function takes two arguments, consisting of tuples of propositions, e.g. `(f, g), (x, y)`. Arbitrary number of arguments is supported.

```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!("");

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)
)
}));
}```

## Modules

 extract Helper utilities for extracting data from proofs.

## Macros

 and An AND relation of variable arguments. bits Evaluates an expression for all bit configurations. bits_format Generates a "{}{}{}..." format for bits. contr Path Semantical Logic: A contractible "family of types". count Counts the number of solutions of a variable argument boolean function. imply An IMPLY chain of variable arguments. or An OR relation of variable arguments. path1_count Path Semantical Logic: Counts the number of solutions of a variable argument boolean function. path1_prove Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. println_bits Prints a truth table with result of a boolean expression. println_extract Prints a truth table extracted from a theory, assigning each case a bit and automatically flip expression properly. prove Returns `true` if proposition is correct, `false` otherwise. tup_count Helper macro for counting size of a tuple. tup_set Helper macro for binding to a tuple pattern. xor An XOR relation of variable 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

 BaseSystem Implemented by base logical systems. Construct Used to construct logical systems. CoreRules Implemented by logical systems to define core rules. Enumerable Implemented by types to use with `all` and `any`. ExtendRules Implemented by logical systems to extend existing ones. Prove Implemented by provable systems of logic.

## Functions

 all Enumerates the type, checking that all outputs are true. and Returns `true` if all arguments are `true`. and3 An 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. path1_count1 Path Semantical Logic: Counts the number of solutions of a 1-argument boolean function, path1_count2 Path Semantical Logic: Counts the number of solutions of a 2-argument boolean function, path1_count3 Path Semantical Logic: Counts the number of solutions of a 3-argument boolean function, path1_count4 Path Semantical Logic: Counts the number of solutions of a 4-argument boolean function, path1_count5 Path Semantical Logic: Counts the number of solutions of a 5-argument boolean function, path1_count6 Path Semantical Logic: Counts the number of solutions of a 6-argument boolean function, path1_count7 Path Semantical Logic: Counts the number of solutions of a 7-argument boolean function, path1_count8 Path Semantical Logic: Counts the number of solutions of a 8-argument boolean function, path1_count9 Path Semantical Logic: Counts the number of solutions of a 9-argument boolean function, path1_count10 Path Semantical Logic: Counts the number of solutions of a 10-argument boolean function, path1_countn Path Semantical Logic: Counts the number of solutions of a n-argument boolean function, path1_countnm Path Semantical Logic: Counts the number of solutions of a n+m-argument boolean function, path1_lennm Path Semantical Logic: Computes number of cases. path1_prove1 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove2 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove3 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove4 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove5 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove6 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove7 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove8 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove9 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_prove10 Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_proven Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. path1_provenm Path Semantical Logic: Returns `true` if proposition is correct, `false` otherwise. 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.