But reasoning in inconsistent knowledge base

1. A method for a processor to respond to a Boolean query using an inconsistent knowledge base, the method comprising:

receiving the Boolean query including an original formula;

determining if the inconsistent knowledge base non-standardly entails the original formula;

when the inconsistent knowledge base non-standardly entails the original formula, selecting a bridge formula that is non-standardly entailed by the inconsistent knowledge base, can be resolved with the original formula, and does not contradict the original formula;

constructing a but answer comprising the original formula, a but formula, and the bridge formula, the but formula being a negation of a resolvent of the original formula and the bridge formula;

validating the but answer; and

transmitting or displaying the but answer with at least the original formula and the but formula.

2. The method of claim 1 , wherein the selecting the bridge formula comprises:

forming the bridge formula as a conjunction of a step number of different clauses in the inconsistent knowledge base;

determining if the original formula and the bridge formula can be resolved;

when the original formula and the bridge formula cannot be resolved so the bridge formula is rejected:

determining if a termination condition is met;

when the termination condition is not met, incrementing the step number and repeating above steps starting from the forming the bridge formula;

when the termination condition is met, ending the method;

when the original formula and the bridge formula can be resolved:

determining if the original formula and the bridge formula are contradictory;

when the original formula and the bridge formula are contradictory so the bridge formula is rejected:

determining if the termination condition is met;

when the termination condition is not met, incrementing the step number and repeating above steps starting from the forming the bridge formula;

when the termination condition is met, ending the method;

when the original formula and the bridge formula are not contradictory, using the bridge formula for the constructing and the validating.

3. The method of claim 2 , wherein the selecting the bridge formula further comprises filtering out the bridge formula when the bridge formula is a conjunction including (1) a prior selected bridge formula, (2) a prior rejected bridge formula that is contradictory with the original formula, or (3) two prior rejected bridge formulas that cannot be resolved with the original formula.

4. The method of claim 2 , wherein the terminal condition comprises one or more of (1) finding one bridge formula, (2) reaching a terminal value for the step number, and (3) going beyond a time period for executing the method.

5. The method of claim 1 , wherein the validating the but answer comprises determining if the inconsistent knowledge base non-standardly entails the but formula, and the but answer is validated when the inconsistent knowledge base non-standardly entails the but formula.

6. The method of claim 1 , further comprising, after the validating the but answer:

determining if a terminal condition is met;

when the termination condition is not met, repeating above steps starting from the selecting;

when the termination condition is met, ending the method.

7. The method of claim 6 , wherein the terminal condition comprises one or more of (1) finding one bridge formula, (2) reaching a terminal value for the step number, and (3) going beyond a time period for executing the method.

8. The method of claim 1 , wherein the transmitting the but answer further includes transmitting the bridge formula with answer and the but formula.

9. The method of claim 1 , wherein non-standardly entailment comprises using a resolution-based selection function to determine, from the inconsistent knowledge base, a subset that standardly entails the but formula, wherein the resolution-based selection function is defined as follows:

rs( , Φ, 0)=Ø

rs( , Φ, 1)={φεK|Φ and φ directly resolvably relevant}

rs( , φ, k)=rs(K, Φ, k)∪{φεK|Φ and φ directly resolvably k-relevant with respect to rs(K, Φ, k−1)}, for k>1.

10. The method of claim 9 , wherein the using the resolution-based selection function comprises:

setting an initial subset and the step value;

using the resolution-based selection function and the step value to add formulas from the inconsistent knowledge base to the subset, the subset extending the initial consistent subset;

determining if the subset is consistent;

when the subset is not consistent:

removing one or more formulas from the subset to make the consistent subset consistent;

determining if the subset classically entails the original formula, wherein:

the inconsistent knowledge base non-standardly entails the original formula when the subset standardly entails the original formula;

the inconsistent knowledge base does not non-standardly entail the original formula when the subset does not standardly entail the original formula;

when the subset is consistent:

determining if the subset is a superset of the initial subset, wherein the inconsistent knowledge base does not non-standardly entail the original formula when the subset is not a superset of the initial subset;

when the subset is a superset of the initial subset:

determining if the subset standardly entails the original formula, wherein the inconsistent knowledge base does non-standardly entails the original formula when the subset standardly entails the original formula;

when the subset does not standardly entail the original formula:

setting the subset as the initial consistent subset, incrementing the step value, and repeating above steps starting from the using the resolution-based selection function and the step value.

11. A non-transitory, computer-readable medium encoded with computer-executable instructions for a processor to implement an inconsistent reasoner that responds to a Boolean query using an inconsistent knowledge base, the instructions comprising:

receiving the Boolean query including an original formula;

determining if the inconsistent knowledge base non-standardly entails the original formula;

when the inconsistent knowledge base non-standardly entails the original formula, selecting a bridge formula that is non-standardly entailed by the inconsistent knowledge base, can be resolved with the original formula, and does not contradict the original formula;

constructing a but answer comprising the original formula, a but formula, and the bridge formula, the but formula being a negation of a resolvent of the original formula and the bridge formula;

validating the but answer; and

transmitting or displaying the but answer with at least the original formula and the but formula.

12. The non-transitory, computer-readable medium of claim 11 , wherein the selecting the bridge formula comprises:

forming the bridge formula as a conjunction of a step number of different clauses in the inconsistent knowledge base;

determining if the original formula and the bridge formula can be resolved;

when the original formula and the bridge formula cannot be resolved so the bridge formula is rejected:

determining if a termination condition is met;

when the termination condition is not met, incrementing the step number and repeating above steps starting from the forming the bridge formula;

when the termination condition is met, ending the method;

when the original formula and the bridge formula can be resolved:

determining if the original formula and the bridge formula are contradictory;

when the original formula and the bridge formula are contradictory so the bridge formula is rejected:

determining if the termination condition is met;

when the termination condition is not met, incrementing the step number and repeating above steps starting from the forming the bridge formula;

when the termination condition is met, ending the method;

when the original formula and the bridge formula are not contradictory, using the bridge formula for the constructing and the validating.

13. The non-transitory, computer-readable medium of claim 12 , wherein the selecting the bridge formula further comprises filtering out the bridge formula when the bridge formula is a conjunction including (1) a prior selected bridge formula, (2) a prior rejected bridge formula that is contradictory with the original formula, or (3) including two prior rejected bridge formulas that cannot be resolved with the original formula.

14. The non-transitory, computer-readable medium of claim 12 , wherein the terminal condition comprises one or more of (1) finding one bridge formula, (2) reaching a terminal value for the step number, and (3) going beyond a time period for executing the method.

15. The non-transitory, computer-readable medium of claim 11 , wherein the validating the but answer comprises determining if the inconsistent knowledge base non-standardly entails the but formula, and the but answer is validated when the inconsistent knowledge base non-standardly entails the but formula.

16. The non-transitory, computer-readable medium of claim 11 , further comprising, after the validating the but answer:

determining if a terminal condition is met;

when the termination condition is not met, repeating above steps starting from the selecting;

when the termination condition is met, ending the method.

17. The non-transitory, computer-readable medium of claim 16 , wherein the terminal condition comprises one or more of (1) finding one bridge formula, (2) reaching a terminal value for the step number, and (3) going beyond a time period for executing the method.

18. The non-transitory, computer-readable medium of claim 11 , wherein the transmitting the but answer further includes transmitting the bridge formula with answer and the but formula.

19. The non-transitory, computer-readable medium of claim 11 , wherein non-standardly entailment comprises using a resolution-based selection function to determine, from the inconsistent knowledge base, a subset that standardly entails the but formula, wherein the resolution-based selection function is defined as follows:

rs( , Φ, 0)=Ø

rs( , Φ, 1)={φεK|Φ and φ directly resolvably relevant}

rs( , Φ, k)=rs(K, Φ, k)∪{φεK|Φ and φ directly resolvably k-relevant with respect to rs(K, Φ, k−1)}, for k>1.

20. The non-transitory, computer-readable medium of claim 19 , wherein the using the resolution-based selection function comprises:

setting an initial subset and the step value;

using the resolution-based selection function and the step value to add formulas from the inconsistent knowledge base to the subset, the subset extending the initial consistent subset;

determining if the subset is consistent;

when the subset is not consistent:

removing one or more formulas from the subset to make the consistent subset consistent;

determining if the subset classically entails the original formula, wherein:

the inconsistent knowledge base non-standardly entails the original formula when the subset standardly entails the original formula;

the inconsistent knowledge base does not non-standardly entail the original formula when the subset does not standardly entail the original formula;

when the subset is consistent:

determining if the subset is a superset of the initial subset, wherein the inconsistent knowledge base does not non-standardly entail the original formula when the subset is not a superset of the initial subset;

when the subset is a superset of the initial subset:

determining if the subset standardly entails the original formula, wherein the inconsistent knowledge base does non-standardly entails the original formula when the subset standardly entails the original formula;

when the subset does not standardly entail the original formula:

setting the subset as the initial consistent subset, incrementing the step value, and repeating above steps starting from the using the resolution-based selection function and the step value.