Expressions

Fundamentally software attempting to both define and prove theorems requires an extensive set of utilities surrounding the function of manipulating expressions. The lowest level of abstraction of expressions in this package is AbstractExpression, from which all expression types inherit from. Anything from symbols to sets are expressions, and a good rule for determining whether something is an expression or not is if it would make mathematical sense to write such an expression down as either a statement or a mathematical object. Logical operations are not expressions since on their own they carry no meaning without arguments.

Logical Symbols

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.

source

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

source

Deductive.name — Method

name(sym::LogicalSymbol)

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

source

Deductive.metadata — Method

metadata(sym::LogicalSymbol)

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

source