Refutation theorem

A refutation theorem is a logical theorem that provides a basis for a chain of deductive conclusions in propositional and predicate logic . Such closing chains are also known as evidence . The refutation theorem forms a complementary formulation of the inference theorem . The refutation theorem has achieved its special importance in the context of an automation of deductive reasoning. It therefore plays a central role in research on artificial intelligence . In detail it says the following:

A formula is a consequence of the formulas if and only if the formula cannot be fulfilled (i.e. inconsistent). ${\displaystyle B}$ ${\displaystyle A_{1},A_{2},...,A_{n}}$ ${\displaystyle A_{1}\wedge A_{2}\wedge ...\wedge A_{n}\wedge {\overline {B}}}$

As Widerlegungsverfahren or Widerlegungskalkül (ger .: refutational calculus ) is called method of proof mathematically -logischer theorems that are based on the Widerlegungstheorem. A statement to be proven is negated and included in an existing set of formulas and an attempt is made to show that the resulting set of formulas cannot be fulfilled.

Well-known refutation procedures are the resolution procedure and the tree calculus .

See also

• Proof of contradiction
• Indirect evidence

literature

Chapter 3 in J. Harrison: Handbook of practical logic and automated reasoning. Cambridge University Press, Cambridge, 2009. ISBN 978-0-521-89957-4