ILogicΒΆ

logic.spad line 2586

parse result includes term returned and new index

/\: (%, %) -> %
from MeetSemilattice
=: (%, %) -> Boolean
returns true (boolean true) if intuitionisticLogic values are the same. Translates from Intuitionistic Logic to Boolean Logic
\/: (%, %) -> %
from JoinSemilattice
_|_: %
from BoundedJoinSemilattice
~: % -> %
~(x) returns the logical complement of x. TODO not sure if complement should be included here? intuitionistic logic can have complement but has different axioms to complement in Boolean algebra. Equivalent capability can be provided by implication.
~=: (%, %) -> Boolean
from BasicType
atom?: % -> Boolean
returns true if this is an atom, that is a leaf node otherwise return false if this is a compound term
coerce: % -> OutputForm
output
deductions: List % -> List %
assumes ln contains a list of factors which must be true for the whole to be true (such as the list produced by factor). From this deductions attempts to produce a list of other proposition that must also be true by using modus ponens. This is used to determine the returned type when converting ILogic to types by using the Curry-Howard isomorphism.
factor: % -> List %
splits n into a list of factors which must be true for the whole to be true. This assumes that the top level is already a set of factors separated by /\ otherwise the result will just be a list with one entry: 'n'. This is used when converting ILogic to types by using the Curry-Howard isomorphism.
getChildren: % -> List %
returns child nodes if this is a compound term otherwise returns []
hash: % -> SingleInteger
from SetCategory
hashUpdate!: (HashState, %) -> HashState
from SetCategory
implies: (%, %) -> %
implies(a, b) returns the logical implication of ILogic a and b. a is premise, b is conclusion, result is false (contradiction) if premise=true and conclusion=false does not mean there is a causal connection
latex: % -> String
from SetCategory
logicF: () -> %
false (contradiction) is a logical constant.
logicT: () -> %
true is a logical constant.
opType: % -> Symbol
if this is a compound op then opType returns the type of that op: “IMPLY”::Symbol =implies “AND”::Symbol=/”OR”::Symbol=\/ “NOT”::Symbol=~ “OTHER”::Symbol=not compound op
parseIL2: (String, NonNegativeInteger) -> Record(rft: %, pout: NonNegativeInteger)
Constructs intuitionistic logic terms from a string notation assumes format like this: <term2> : := var | “(“<term>”)” <term> : := var | <term>/\<term> | <term>\/<term> | <term>-><term> | “(“<term>”)”
parseIL: String -> %
Constructs intuitionistic logic terms from a string notation assumes format like this: <term> : := var | <term>/\<term> | <term>\/<term> | <term>-><term> | “(“<term>”)”
parseILTerm: (String, NonNegativeInteger) -> Record(rft: %, pout: NonNegativeInteger)
parseTerm is used by parseIL. It would rarely be called externally but it is here to allow it to call parseIL that is to allow circular calls
proposition: String -> %
Constructs a proposition
redux: % -> %
attempt to simplify theory apply recursively to subnodes normally this should not be necessary since logic values are interpreted when constructed
T: %
from BoundedMeetSemilattice
toString: % -> String
creates a string representation of this term and its sub-terms
toStringUnwrapped: % -> String
similar to ‘toString’ but does not put outer compound terms in brackets
value: % -> Symbol
returns: “T”::Symbol = T “F”::Symbol = _|_ “E”::Symbol = error “P”::Symbol = proposition “C”::Symbol = compound Constructs lambda term and bind any variables with the name provided

BasicType

BoundedJoinSemilattice

BoundedLattice

BoundedMeetSemilattice

CoercibleTo OutputForm

JoinSemilattice

MeetSemilattice

SetCategory