[][src]Crate pocket_prover

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

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.