## Deductive.jl

A package for expressing and automatically proving logical statements symbolically in Julia
Author ctrekker
Popularity
20 Stars
Updated Last
1 Year Ago
Started In
December 2021

# Deductive.jl

Deductive is a package for expressing and proving zeroth order and first order logical statements and theorems symbolically in Julia.

## Installation

Currently this package is unregistered in Julia's general registry. Instead install through this repository directly.

(@v1.7) pkg> add https://github.com/ctrekker/PropositionalLogic.jl


## Getting Started

### Propositional Logic (zeroth order)

using Deductive

@symbols a b

tableau(a ∧ b)      # true
tableau(a ∧ b, ¬a)  # false, because contradiction

println(truthtable(a ∧ b))
#= Outputs:
Row │ a      b      a ∧ b
│ Bool   Bool   Bool
─────┼─────────────────────
1 │ false  false  false
2 │  true  false  false
3 │ false   true  false
4 │  true   true   true
=#

Several operators are exported and their use is required in defining statements.

Symbol Completion Sequence Description
¬ \neg Negation
\wedge Logical Conjunction
\vee Logical Disjunction
\rightarrow Material Implication
\leftrightarrow Material Equivalence

### OUTDATED Predicate Logic (first order)

With predicates, statements like "for all x, P(x) is true" can be written. Due to some Julia parser issues, defining a function with the symbols for universal (∀) and existential (∃) quantification isn't possible. Instead we settle for the symbols Ā (typed A\bar) and Ē (typed (E\bar)). Here's an example of their use:

using Deductive

x = FreeVariable(:x)
P = Proposition(:P)

Ā(x, P(x))  # like saying "for all x, P(x) is true"
Ē(x, P(x))  # like saying "for some x, P(x) is true"
¬Ē(x, ¬P(x))  # like saying "there does not exist x such that P(x) is false", which is equivalent to Ā(x, P(x))

As an interesting example, the equivalence between Ā(x, P(x)) and ¬Ē(x, ¬P(x)) can be proven as a tautology within this package using the tableau function. This logical equivalence can be expressed as a statement Ā(x, P(x)) ⟷ ¬Ē(x, ¬P(x)), or "for all x, P(x) is true if and only if there does not exist any x such that P(x) is false".

using Deductive

x = FreeVariable(:x)
P = Proposition(:P)

my_statement = Ā(x, P(x)) ⟷ ¬(Ē(x, ¬P(x)))
tableau(¬my_statement)  # returns false, since the contradiction of a tautology is always false

The method of analytic tableaux is a complete method for proving zeroth and first order logic problems. To export these proofs in human-readable form the prove function is exported. Instead of simply yielding a true or false, this function will return a full proof containing the steps taken to determine whether a set of propositions are consistent.

using Deductive

@symbols a b c d

# basic example from above
prove(a ∧ b, ¬a)
#= Output:
┌─────────────┬───────────┬────────────────┬────────────┐
│ Line Number │ Statement │       Argument │ References │
│       Int64 │    String │         String │     String │
├─────────────┼───────────┼────────────────┼────────────┤
│           1 │     a ∧ b │     Assumption │            │
│           2 │      ¬(a) │     Assumption │            │
│           3 │         a │ Simplification │          1 │
│           4 │         b │ Simplification │          1 │
│           5 │  a ∧ ¬(a) │  Contradiction │       3, 2 │
└─────────────┴───────────┴────────────────┴────────────┘
=#

# a far more fun example :)
prove(a → b, b → c, c → d, a, ¬d)
#= Output:
┌─────────────┬──────────────────────────┬─────────────────────────┬────────────┐
│ Line Number │                Statement │                Argument │ References │
│       Int64 │                   String │                  String │     String │
├─────────────┼──────────────────────────┼─────────────────────────┼────────────┤
│           1 │                    a → b │              Assumption │            │
│           2 │                    b → c │              Assumption │            │
│           3 │                    c → d │              Assumption │            │
│           4 │                        a │              Assumption │            │
│           5 │                     ¬(d) │              Assumption │            │
│           6 │                 ¬(c) ∨ d │ Replacement Rule <TODO> │            │
│           7 │                 ¬(a) ∨ b │ Replacement Rule <TODO> │            │
│           8 │                 ¬(b) ∨ c │ Replacement Rule <TODO> │            │
│           9 │                     ¬(c) │                  Case 1 │          6 │
│          10 │                        d │                  Case 2 │          6 │
│          11 │                     ¬(a) │                  Case 1 │          7 │
│          12 │                        b │                  Case 2 │          7 │
│          13 │                 a ∧ ¬(a) │           Contradiction │      4, 11 │
│          14 │                     ¬(b) │                  Case 1 │          8 │
│          15 │                        c │                  Case 2 │          8 │
│          16 │                 b ∧ ¬(b) │           Contradiction │     12, 14 │
│          17 │                 c ∧ ¬(c) │           Contradiction │      15, 9 │
│          18 │ ¬(¬(b) ∨ c) ∧ (¬(b) ∨ c) │           Contradiction │     14, 15 │
│          19 │ ¬(¬(a) ∨ b) ∧ (¬(a) ∨ b) │           Contradiction │     11, 12 │
│          20 │                 d ∧ ¬(d) │           Contradiction │      10, 5 │
│          21 │ ¬(¬(c) ∨ d) ∧ (¬(c) ∨ d) │           Contradiction │      9, 10 │
└─────────────┴──────────────────────────┴─────────────────────────┴────────────┘
=#

As is clear from the second example, several arguments are missing regarding replacement rules, and the organization is rather poor. This feature is very much work in progress right now.

### Required Packages

View all packages

### Used By Packages

No packages found.