Crate pocket_prover

Expand description

§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: {}", 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)
        )
    }));
}

§Path Semantical Quality

Pocket-Prover has a model of Path Semantical Quality that resembles quantum logic.

To write x ~~ y you use q(x, y) or qual(x, y).

q(x, y) is the same as and!(eq(x, y), qubit(x), qubit(y)). q(x, x) is the same as qubit(x).

A qubit is a kind of “superposition”. One can also think about it as introducing a new argument qubit(x) that depends on x.

Since qubits can collide with other propositions, one must repeat measurements e.g. using measure to get classical states. However, sometimes one might wish to amplify quantum states, using amplify or amp.

To use quality with path semantics, one should use ps_core. Path Semantical Logic is designed for equality, not quality.

use pocket_prover::*;

fn main() {
    println!("Path semantics: {}", measure(1, || prove!(&mut |a, b, c, d| {
        imply(
            and!(
                ps_core(a, b, c, d),
                imply(a, c),
                imply(b, d)
            ),
            imply(qual(a, b), qual(c, d))
        )
    })));
}

Re-exports§

pub use qual as q;
pub use qubit as qu;
pub use aqual as aq;
pub use contra_qual as cq;
pub use platonic_qubit as pqu;
pub use amplify as amp;

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.
Observable: Implemented by observables.
Prove: Implemented by provable systems of logic.

Functions§

all: Enumerates the type, checking that all outputs are true.
amplify: Amplify a “wavefunction” of a proposition using its qubit transform.
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.
aqual: Path semantical aquality a ~¬~ b.
cont: Path semantical continuous map a ~> b.
contra_qual: Path semantical contravariant quality a ¬~~ b.
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.
hom_and: Aligns logical AND of qubits up to some homotopy level.
hom_eq: Aligns equality of qubits up to some homotopy level.
hom_f: Path semantical function f_n(a, b) up to some homotopy level n.
hom_imply: Aligns implication of qubits up to some homotopy level.
hom_or: Aligns logical OR of qubits up to some homotopy level.
hom_xor: Aligns logical XOR of qubits up to some homotopy level.
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.
is_groupoid: Defines a groupoid relation from x to a and b.
is_groupoid_n: Defines an n-groupoid relation from x to a and b.
is_hom_lev_n: Defines a homotopy level n relation from x to a and b.
is_prop: Defines a proposition relation of proposition x to potential proofs a and b.
is_set: Defines a set relation from a set x to potential members a and b.
measure: Measures result repeatedly.
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.
platonic_qubit: Prepares a platonic qubit using a proposition as seed.
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.
ps_acore: Assumes the path semantical acore axiom.
ps_acore_eq: Assumes a strong version of the path semantical acore axiom.
ps_core: Assumes the path semantical core axiom.
ps_core_eq: Assumes a strong version of the path semantical core axiom.
ps_sym_core: Assumes the symmetric path semantical core axiom.
ps_sym_core_eq: Assumes a strong version of the symmetric path semantical core axiom.
qual: Path semantical quality a ~~ b.
qubit: Prepares a qubit using a proposition as seed.
re_sesh: Restore Sesh property to a proposition.
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.
un_sesh: Removes Sesh property from a proposition.
univ: Assumes univalence axiom for some homotopy level.
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 Aliases§

Pred1: A boolean function of one argument.
Pred2: A boolean function (transformed) of two arguments.

Crate pocket_proverCopy item path