¬(x)

Logical negation operator, typed with \neg. Boolean equivalent is the ! operator.

x → y

Logical implication operator, typed with \rightarrow.

x ∧ y

Logical conjunction operator, typed with \wedge. Boolean equivalent is the && operator.

x ∨ y

Logical disjunction operator, typed with \vee. Boolean equivalent is the || operator.

A ⊢ B

Provability operator used exclusively in calculus definitions. A ⊢ B means that B can be proven using A as the premise.

a ⊼ b

Not AND operator (NAND for short). The NAND operator is a functionally complete boolean operator, meaning all other boolean operations can be expressed with only NAND operations.

x ⟷ y

Logical equivalence operator, typed with \longleftrightarrow.

PropositionalCalculus

Default calculus definition for zeroth-order (propositional) logic.

AbstractExpression

The abstract type which all expression trees are built from.

FakeVector{X, T}(creator::X, fieldname::Symbol, vec::Vector{T})

A utility structure which calls a function setvectorindex! when the Base.setindex! function is called on it. This allows for some smart updating of expression trees when mutated.

InferenceRule(name::String, premise::StatementSet, conclusion::Statement)

Define a rule which maps a set of statements to a logical conclusion. The name is cited each time a rule is applied in a proof step.

LogicalExpression(arguments::Vector{AbstractExpression}, operation::LogicalOperation)

Constructs an expression with given arguments and logical operation. Please refrain from using this syntax, instead using the "operators as functions" syntax, where a LogicalOperation instance can be called to produce a LogicalExpression.

LogicalOperation(bool_fn::Function, name::Symbol, argument_count::Int, associative::Bool, commutative::Bool)

Defines a logical operator which can be used to form expressions with. Usually you don't need to define your own operators, just use the ones built-in to the package if possible.

(op::LogicalOperation)(args::AbstractExpression...)

This function is the foundation of expression building, as it allows instances of LogicalOperations to be treated as real Julia functions. When called this function returns a LogicalExpression representing the application of the given operator on the provided arguments.

LogicalSymbol(name::Symbol, metadata::Any=nothing)

Represent a logical symbolically with a provided name. By default the attached metadata is set to nothing.

add_to_parents!(expr::LogicalExpression)

Adds an expression to the parents set of all its arguments. For internal use only.

argument_count(op::LogicalOperation)

The number of arguments which the given operation expects to receive.

arguments(expr::T) where {T <: AbstractExpression}

Returns the arguments which an AbstractExpression contains. LogicalSymbols contain no arguments and LogicalExpressions can contain any number of arguments.

associative_ordering(expr::LogicalExpression)

Descends the expression tree with a left-side-first depth first search. Each symbol encountered is added to a list in the order it appears in this search and is returned by this function.

associative_tree_count(nodes::Int)

Function which calculates how many ways to arrange parenthesis in an expression there are with a given node count.

contains_expression(haystack::AbstractExpression, kneedle::AbstractExpression)

Searches for a subexpression kneedle recursively within the haystack expression. Returns true if a match can be found and false otherwise.

flat_repeat(x, n)

Shortcut for Iterators.repeat([x], n)

isassociative(expr::LogicalExpression)

Checks if the entire expression is associative based on the associative property of its constituent operations.

isassociative(op::LogicalOperation)

True if the given operation is associative, false otherwise.

isbinary(op::LogicalOperation)

True if the given operation receives two arguments, false otherwise.

iscommutative(expr::LogicalExpression)

Checks if the entire expression is commutative based on the commutative property of its constituent operations.

iscommutative(op::LogicalOperation)

True if the given operation is commutative, false otherwise.

isequal_associative(expr1::LogicalExpression, expr2::LogicalExpression)

Checks whether an expression is equal with another ignoring the associative ordering of each expression.

isnode(expr::T) where {T <: AbstractExpression}

Returns true when expr is a LogicalSymbol and false otherwise.

istree(expr::T) where {T <: AbstractExpression}

Returns true when expr is a LogicalExpression and false otherwise.

isunary(op::LogicalOperation)

True if the given operation only receives one argument, false otherwise.

left(expr::LogicalExpression)

If the expression is binary, this method returns the left-hand operand.

metadata(sym::LogicalSymbol)

The metadata of the symbol provided at instantiation, if any. Returns nothing if none was provided.

name(sym::LogicalSymbol)

The name of the symbol provided at instantiation. Equivalent to symbol(sym).

operation(expr::LogicalExpression)

The operation which is performed on the arguments of the given LogicalExpression.

operations(expr::T) where {T <: AbstractExpression}

Returns the operations present in an entire expression tree. When given a LogicalSymbol, this is an empty set, whereas when given a LogicalExpression, this is a set containing the expression's own LogicalOperation and the operations set of each of its arguments.

parents(expr::LogicalExpression)

The parent expressions of a given subexpression. If an expression is never used within another, it will have no parents. In most expressions there will only be one parent, but it is possible for an expression assigned to a variable to have multiple parents by using it as a "named subexpression".

remove_from_parents!(expr::LogicalExpression)

Removes an expression from the parents set of all its arguments. For internal use only.

right(expr::LogicalExpression)

If the expression is binary, this method returns the right-hand operand.

variables(expr::T) where {T <: AbstractExpression}

Returns variables present in an entire expression tree. When the first argument is a LogicalSymbol, this is singleton set containing only the provided LogicalSymbol. When the argument is a LogicalExpression, this is a set containing the union of all the variables present in each argument.

Defines a logical calculus based on a set of inference rules which can be applied repeatedly to a given set of statements (premises). See PropositionalCalculus for an example definition using this macro.

Define any number of LogicalSymbols with the names provided.

Examples

julia> @symbols a  # defines symbol `a` in the current scope

julia> @symbols b c d  # defines symbols `a`, `b`, and `c`

julia> @symbols α β γ  # defines symbols `α`, `β`, and `γ`