Architecture for an artificial agent that reasons defeasibly

A computer implemented method for defeasible reasoning, comprising the steps of:

• (a) generating a list of conclusions by monotonic reasoning and recording said conclusions in a selected one of a simple inference-graph and an and/or inference graph each having nodes corresponding to said conclusions:
• (b) computing defeat-statuses for said nodes of said inference-graph, using a method comprising the steps of:
• (i) computing a list of status-assignments;
• (ii) computing the defeat-status of a selected node by employing a method selected from the group consisting of:
• (A) a method for computing the defeat-status of a selected node wherein said inference-graph is an and/or inference-graph and said node is judged undefeated only if every status-assignment assigns a nonzero defeat status to said node;
• and
• (B) a method for computing the defeat-status of a selected node wherein said inference-graph is an and/or inference-graph and said node is judged undefeated if said inference-graph contains nodes that constitute an argument for said node and all of said nodes in said argument are assigned an undefeated defeat-status by every status-assignment;
• (c) through the use of monotonic reasoning, selecting a set of sequents in a list input, and a set of sequents in a list ultimate-epistemic-interests;
• (d) categorizing said sequents in said list input as conclusions and inserting sequents into an ordered list inference-queue;
• (e) categorizing said sequents in said list ultimate-epistemic-interests as interests and inserting said interests into said list inference-queue;
• (f) retrieving in order said conclusions and said interests of said list inference-queue;
• (g) for each said conclusion retrieved, performing forward reasoning to produce new conclusions and storing said new conclusions in a data structure inference-graph and also placing said new conclusions on said list inference-queue;
• (h) for each said interest retrieved performing, backward reasoning to produce new interests and storing said new interests in a data structure interest-graph and also placing said new interests list on said list inference-queue;
• (i) comparing each said new conclusion with said interests recorded in said interest-graph and discharging from said inference graph each said new conclusion that is the same as an interest recorded in said interest graph;
• and
• (j) comparing each said new interest with said conclusions recorded in the inference-graph, and discharging from said interest graph each said new interest that is the same as a conclusion recorded in said inference graph.

A computer implemented method for reasoning, comprising the steps of:

• (a) using forward-inference rules EI and UI and backward-logical reasons EG and UG to skolemize interest-formulas and conclusion formulas;
• (b) using unification to compute common instances of forwards-reasons and the node-formulas in inference-nodes, and using unification to compute conclusions to be inferred from said inference-nodes in accordance with said forwards-reasons;
• (c) when a supposition is generated by an interest, the interest-variables of the interest are made the node-variables of the inference-node recording the supposition;
• and
• (d) discharging interests by unifying the node-formula of an inference-node and the interest-formula of an interest to produce a unifier, applying said unifier to their suppositions, and then unifying the resulting node-supposition into the resulting interest-supposition.

A computer implemented method for reasoning, comprising the steps of:

• (a) using procedure adopt-reductio-interest to create reductio-interests having schematic supposition;
• and
• (b) using procedures discharge reductios and
• discharge-retrospective-reductios to discharge reductio-interests having schematic suppositions.