Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Prover9
Résumé
Prover9 is an automated theorem prover for first-order and equational logic developed by William McCune.
Prover9 is the successor of the Otter theorem prover also developed by William McCune. Prover9 is noted for producing relatively readable proofs and having a powerful hints strategy.
Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples. Both can be run simultaneously from the same input, with Prover9 attempting to find a proof, while Mace4 attempts to find a (disproving) counter-example. Prover9, Mace4, and many other tools are built on an underlying library named LADR ("Library for Automated Deduction Research") to simplify implementation. Resulting proofs can be double-checked by Ivy, a proof-checking tool that has been separately verified using ACL2.
In July 2006 the LADR/Prover9/Mace4 input language made a major change (which also differentiates it from Otter). The key distinction between "clauses" and "formulas" completely disappeared; "formulas" can now have free variables; and "clauses" are now a subset of "formulas". Prover9/Mace4 also supports a "goal" type of formula, which is automatically negated for proof. Prover9 attempts to automatically generate a proof by default; in contrast, Otter's automatic mode must be explicitly set.
Prover9 was under active development, with new releases every month or every other month, until 2009. Prover9 is free software, and therefore, open source software; it is released under GPL version 2 or later.
The traditional "all men are mortal", "Socrates is a man", prove "Socrates is mortal" can be expressed this way in Prover9:
formulas(assumptions).
man(x) -> mortal(x). % open formula with free variable x
man(socrates).
end_of_list.
formulas(goals).
mortal(socrates).
end_of_list.
This will be automatically converted into clausal form (which Prover9 also accepts):
formulas(sos).
man(x) | mortal(x).
man(socrates).
mortal(socrates).
end_of_list.
A proof that the square root of 2 is irrational can be expressed this way:
formulas(assumptions).
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Cours associés (26)
MATH-205: Analysis IV
Learn the basis of Lebesgue integration and Fourier analysis
CS-101: Advanced information, computation, communication I
Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a
MATH-351: Advanced numerical analysis
The student will learn state-of-the-art algorithms for solving differential equations. The analysis and implementation of these algorithms will be discussed in some detail.
Séances de cours associées (46)
Formes harmoniques et surfaces de Riemann
Explore les formes harmoniques sur les surfaces de Riemann, couvrant l'unicité des solutions et l'identité bilinéaire de Riemann.
Formule d'inversion de Fourier
Couvre la formule d'inversion de Fourier, explorant ses concepts mathématiques et ses applications, soulignant l'importance de comprendre le signe.
Formes harmoniques : théorème principal
Explore les formes harmoniques sur les surfaces de Riemann et l'unicité des solutions aux équations harmoniques.
Publications associées (32)
Transportation-based functional ANOVA and PCA for covariance operators
Victor Panaretos, Yoav Zemel, Valentina Masarotto
We consider the problem of comparing several samples of stochastic processes with respect to their second-order structure, and describing the main modes of variation in this second order structure, if present. These tasks can be seen as an Analysis of Vari ...
Inst Mathematical Statistics-Ims2024Automated Formal Verification of Software Network Functions
Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...
EPFL2024A semantic model-based systems engineering approach for assessing the operational performance of metal forming process
Metal Forming is a basic and essential industrial process to provide materials for constructing complex products. To design an efficient metal forming process, the functional requirements and operational performance are two important aspects to be consider ...
Pergamon-Elsevier Science Ltd2024Personnes associées (2)
Concepts associés (1)
Démonstration automatique de théorèmes
La démonstration automatique de théorèmes (DAT) est l'activité d'un logiciel qui démontre une proposition qu'on lui soumet, sans l'aide de l'utilisateur. Les démonstrateurs automatiques de théorème ont résolu des conjectures intéressantes difficiles à établir, certaines ayant échappé aux mathématiciens pendant longtemps ; c'est le cas, par exemple, de la , démontrée en 1996 par le logiciel EQP.