Système de preuve interactivevignette|504x504px|Un système de preuve interactive est composé de deux machines abstraites : un prouveur et un vérificateur qui s'échangent des messages. En théorie de la complexité des algorithmes, un système de preuve interactive est un protocole formel de démonstration de théorèmes qui fait intervenir deux participants qui échangent des messages. Cela permet de définir des classes de complexité intéressantes, notamment la classe IP qui est le modèle utilisé dans le théorème PCP qui caractérise la classe NP.
Démonstration (logique et mathématiques)vignette| : un des plus vieux fragments des Éléments d'Euclide qui montre une démonstration mathématique. En mathématiques et en logique, une démonstration est un ensemble structuré d'étapes correctes de raisonnement. Dans une démonstration, chaque étape est soit un axiome (un fait acquis), soit l'application d'une règle qui permet d'affirmer qu'une proposition, la conclusion, est une conséquence logique d'une ou plusieurs autres propositions, les prémisses de la règle.
Computer-assisted proofA computer-assisted proof is a mathematical proof that has been at least partially generated by computer. Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical theorem. The idea is to use a computer program to perform lengthy computations, and to provide a proof that the result of these computations implies the given theorem. In 1976, the four color theorem was the first major theorem to be verified using a computer program.
ArgumentationL’argumentation est l'action de convaincre et pousser ainsi l'autre à agir. Contrairement à la persuasion, elle vise à être comprise de tous et résiste à l'utilisation d'arguments fallacieux. L’argument est, en logique et en linguistique, l’ensemble des prémisses données en support à une conclusion. Une argumentation est composée d'une conclusion et d'un ou de plusieurs « éléments de preuve », que l'on appelle des prémisses ou des arguments, et qui constituent des raisons d'accepter cette conclusion.
Argument ontologiqueL'argument ontologique est un argument qui vise à prouver l'existence de Dieu. Il est dit ontologique, car il appuie sa preuve sur la définition de ce qu'est l'être (ontos) de Dieu : il est dans l'être de Dieu d'exister. On considère généralement que Boèce () est le premier à avoir proposé un argument de ce genre, mais c'est sa formulation par Anselme de Cantorbéry au qui rend l'argument célèbre. À l'époque moderne, la version cartésienne de l'argument a été particulièrement influente, faisant l'objet de plusieurs critiques qui conduisent à rejeter la valeur des arguments ontologiques en général.
