`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.PropositionalCalculus`

— Constant`PropositionalCalculus`

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

`Deductive.AbstractExpression`

— Type`AbstractExpression`

The abstract type which all expression trees are built from.

`Deductive.FakeVector`

— Type`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.InferenceRule`

— Type`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.LogicalExpression`

— Type`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.LogicalOperation`

— Type`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.LogicalOperation`

— Method`(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.LogicalSymbol`

— Type`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.argument_count`

— Method`argument_count(op::LogicalOperation)`

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

`Deductive.arguments`

— Method`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_ordering`

— Method`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_count`

— Method`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_expression`

— Method`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.flat_repeat`

— Method`flat_repeat(x, n)`

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

`Deductive.isassociative`

— Method`isassociative(expr::LogicalExpression)`

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

`Deductive.isassociative`

— Method`isassociative(op::LogicalOperation)`

True if the given operation is associative, false otherwise.

`Deductive.isbinary`

— Method`isbinary(op::LogicalOperation)`

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

`Deductive.iscommutative`

— Method`iscommutative(expr::LogicalExpression)`

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

`Deductive.iscommutative`

— Method`iscommutative(op::LogicalOperation)`

True if the given operation is commutative, false otherwise.

`Deductive.isequal_associative`

— Method`isequal_associative(expr1::LogicalExpression, expr2::LogicalExpression)`

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

`Deductive.isnode`

— Method`isnode(expr::T) where {T <: AbstractExpression}`

Returns true when `expr`

is a `LogicalSymbol`

and false otherwise.

`Deductive.istree`

— Method`istree(expr::T) where {T <: AbstractExpression}`

Returns true when `expr`

is a `LogicalExpression`

and false otherwise.

`Deductive.isunary`

— Method`isunary(op::LogicalOperation)`

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

`Deductive.left`

— Method`left(expr::LogicalExpression)`

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

`Deductive.metadata`

— Method`metadata(sym::LogicalSymbol)`

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

if none was provided.

`Deductive.name`

— Method`name(sym::LogicalSymbol)`

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

.

`Deductive.operation`

— Method`operation(expr::LogicalExpression)`

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

.

`Deductive.operations`

— Method`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.parents`

— Method`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.right`

— Method`right(expr::LogicalExpression)`

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

`Deductive.variables`

— Method`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_calculus`

— MacroDefines 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.@symbols`

— MacroDefine 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 `γ`
```