
Justifications
This document is: [JUSTIFICATION]
To set the stage, justifications occur: 1) in logic, where. for example, in natural deduction
a proof tree is annotated with the rules used at each node and so 'justifies' the end formula;
and 2) in AI in the form of 'assumption based reasoning', which has been developed to simplify
'truth maintenance' systems.
We allow for many types of justifications and they can have many different forms. The details
do not become important until we introduce the notion of consequence and a facility to reason
about them. Some examples might be 'I am in the facts of C as an assumption because my wff
is an axiom of group theory', 'I am in the facts of C as an assumption because Fred was on
LSD and he thought my wff was a good idea', 'I am in the facts of C as a conclusion because
my wff is a consequence of using the rule of inference R on fact1 and fact2', etc. Justifications
can be as exotic as you can imagine but are meant to be the record of why a wff had been included
as a fact in its context.
We use the analysis of justifications as defined in natural deduction (taken together with the
results of interpretating expressions in a simulation structure) to make conclusions
from a context and as a reason for sometines adding a fact concluded from a context
TO THE >B>CONTEXT.
The type of a justification is
(focus C
(type [justification] subtype []
(description :type [string]) ) )