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
— TypeLogicalSymbol(name::Symbol, metadata::Any=nothing)
Represent a logical symbolically with a provided name. By default the attached metadata is set to nothing
.
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 `γ`
Deductive.name
— Methodname(sym::LogicalSymbol)
The name of the symbol provided at instantiation. Equivalent to symbol(sym)
.
Deductive.metadata
— Methodmetadata(sym::LogicalSymbol)
The metadata of the symbol provided at instantiation, if any. Returns nothing
if none was provided.