Proof by contradiction - artificial intelligence, Computer Engineering

Assignment Help:

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


Related Discussions:- Proof by contradiction - artificial intelligence

Basic operational concepts of a computer, Basic Operational Concepts of a C...

Basic Operational Concepts of a Computer: Most of computer operations are executed in the ALU (arithmetic and logic unit) of a processor. For an example: to add 2 numb

Data, Data, information and knowledge - Information System The nature ...

Data, information and knowledge - Information System The nature of information can most easily be defined in the context of its relationship to data and knowledge. Bohn (1994)

What is overflow and underflow case in single precision, What is overflow, ...

What is overflow, underflow case in single precision(sp)? Underflow-In SP it means that the normalized representation needs an exponent less than -126. Overflow-In SP it mea

What are the uses of interrupts, What are the uses of interrupts?  ...

What are the uses of interrupts?  Recovery from errors Debugging Communication among programs Use of interrupts in operating system

What is dialog module, What is dialog Module? A dialog Module is a call...

What is dialog Module? A dialog Module is a callable sequence of screens that does not belong to a certain  transaction. Dialog modules have their module pools, and can be know

Differences between a database index and a match code, What are the differe...

What are the differences between a Database index and a match code? Match code can have fields from several tables whereas an index can have fields from only one table.

What is interrupt vector table, Interrupt vector table is always created in...

Interrupt vector table is always created in first 1K area of the memory. Explain why? When CPU receives an interrupt type number from PIC, it uses this number to look up corres

Pvm communication model, Q. PVM communication model? A nonblocking rece...

Q. PVM communication model? A nonblocking receive as soon as returns with either data or a flag that data hasn't arrived while a blocking receive returns only when data is in r

Write Your Message!

Captcha
Free Assignment Quote

Assured A++ Grade

Get guaranteed satisfaction & time on delivery in every assignment order you paid with us! We ensure premium quality solution document along with free turntin report!

All rights reserved! Copyrights ©2019-2020 ExpertsMind IT Educational Pvt Ltd