Proof by contradiction - artificial intelligence, Computer Engineering

Proof by Contradiction - Artificial intelligence

So, both backward chaining andforward chaining have drawbacks. Another approach is to think regarding proving theorems by contradiction. These are so much common in mathematics: mathematicians specify some axioms, and then make an assumption. After some complexes mathematics, they have proven that an axiom is  false  (or  something  derived  from  the  axioms  which  did  not  involve  the assumption is false). As the axioms are irrefutably right, this means that the assumption they made might be false. That is, the assumption is not consistent with the axioms of the theory. To utilize this for a specific theorem which they want to prove is true; they negate the theorem statement and use this as the assumption they are going to display is false. As the negated theorem must be false, their original theorem ought to be true.

We may program our reasoning agents to do just the similar.Therefore, to specify this as a search problem, we need to say that the axioms of our theory and the negation of the theorem we want to prove are the starting search states. Recalling our example in section, to do this, we have to derive the false statement to show inconsistency, that the reason that the False statement becomes our goal. So, if we can deduce the false statement from our axioms, the theorem we were attempting to prove will certainly have been proven. This means that, not only can we use all our rules of inference; we also have goal to aim for.

As an instance, below is the input to the Otter theorem proves for the trivial theorem regarding Socrates being mortal. Otter searches for contradictions by using resolution, hence we notice that the theorem statement that Socrates is mortal is negated  byusing the minus sign.

Input:

set(auto). formula_list(usable).

all x (man(x)->mortal(x)). % for all x, if x is man then x is mortal

man(socrates). % Socrates is man

-mortal(socrates).        % Socrates is immortal (note: negated)

end_of_list.

Otter has no problem whatsoever proving this theorem, and output is following:

Output:

 PROOF

1 [] -man(x)|mortal(x).

2 [] -mortal(socrates).

3 [] man(socrates).

4 [hyper,3,1] mortal(socrates).

5 [binary,4.1,2.1] $F.

Hence  proof

Posted Date: 10/2/2012 8:32:32 AM | Location : United States







Related Discussions:- Proof by contradiction - artificial intelligence, Assignment Help, Ask Question on Proof by contradiction - artificial intelligence, Get Answer, Expert's Help, Proof by contradiction - artificial intelligence Discussions

Write discussion on Proof by contradiction - artificial intelligence
Your posts are moderated
Related Questions
Q. Explain about working of Multiplexer? Multiplexer is one of the fundamental building units of a computer system that in principle permits sharing of a common line by more th

Amdahl's law is suitable for applications where response time is critical. On the other hand, there are a lot of applications which need that accuracy of the resultant output shoul

Q. How to Transmits data in the active message buffer? int pvm_bcast( char *group, int msgtag ) Transmits data in the active message buffer to a group of processes. msgt

1. Design a DTD for a new XML application called Library Markup Language (LibML) appropriate to capture the list of your items of collection . Put the DTD into a file named librar

An off-hook signal will repeat for a/an                   duration. For a/an finite duration, an off-hook signal will repeat.

ANN Representation: Mostly 'ANNs' are taught on "AI" courses since their motivation from brain studies and the fact which they are used in an "AI" task and namely machine lear

Q. Standards for scan codes ? There are 3 standards for scan codes: Mode1 (83-key keyboard PC, PC-XT) and Mode2 (84-key AT keyboard) and Mode3 (101-key keyboard onwards). In Mo

When a window is repainted by the AWT painting thread, it sets the clipping regions to the area of the window that needs repainting.

Q. Use of Intrinsic Functions in FORTRAN? HPF initiates some new intrinsic functions also to those defined in F90. The two mainly often used in parallel programming are system

Define the terms- Action Semantics and  ArgoUML Action Semantics : Action semantics is a group of firms that have responded to the OMG's RFP to define the action semantics fo