Deductive.:¬Constant
¬(x)

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

Deductive.:→Constant
x → y

Logical implication operator, typed with \rightarrow.

Deductive.:∧Constant
x ∧ y

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

Deductive.:∨Constant
x ∨ y

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

Deductive.:⊢Constant
A ⊢ B

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

Deductive.:⊼Constant
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.

Deductive.:⟷Constant
x ⟷ y

Logical equivalence operator, typed with \longleftrightarrow.

Deductive.FakeVectorType
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.

Deductive.InferenceRuleType
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.

Deductive.LogicalExpressionType
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.

Deductive.LogicalOperationType
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.

Deductive.LogicalOperationMethod
(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.

Deductive.LogicalSymbolType
LogicalSymbol(name::Symbol, metadata::Any=nothing)

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

Deductive.add_to_parents!Method
add_to_parents!(expr::LogicalExpression)

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

Deductive.argumentsMethod
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.

Deductive.associative_orderingMethod
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.

Deductive.associative_tree_countMethod
associative_tree_count(nodes::Int)

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

Deductive.contains_expressionMethod
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.

Deductive.isassociativeMethod
isassociative(expr::LogicalExpression)

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

Deductive.isbinaryMethod
isbinary(op::LogicalOperation)

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

Deductive.iscommutativeMethod
iscommutative(expr::LogicalExpression)

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

Deductive.isequal_associativeMethod
isequal_associative(expr1::LogicalExpression, expr2::LogicalExpression)

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

Deductive.isnodeMethod
isnode(expr::T) where {T <: AbstractExpression}

Returns true when expr is a LogicalSymbol and false otherwise.

Deductive.istreeMethod
istree(expr::T) where {T <: AbstractExpression}

Returns true when expr is a LogicalExpression and false otherwise.

Deductive.isunaryMethod
isunary(op::LogicalOperation)

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

Deductive.leftMethod
left(expr::LogicalExpression)

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

Deductive.metadataMethod
metadata(sym::LogicalSymbol)

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

Deductive.nameMethod
name(sym::LogicalSymbol)

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

Deductive.operationMethod
operation(expr::LogicalExpression)

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

Deductive.operationsMethod
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.

Deductive.parentsMethod
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".

Deductive.remove_from_parents!Method
remove_from_parents!(expr::LogicalExpression)

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

Deductive.rightMethod
right(expr::LogicalExpression)

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

Deductive.variablesMethod
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.

Deductive.@logical_calculusMacro

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.

Deductive.@symbolsMacro

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 γ