automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...

, PhoX is a

proof assistant In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof edi ...

based on

higher-order logic In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...

which is eXtensible. The user gives PhoX an initial goal and guides it through subgoals and evidence to prove that goal; internally, it constructs natural deduction trees. Each previously proven formula can become a rule for later proofs. PhoX was originally designed and implemented by

Christophe Raffalli Christophe may refer to: People * Christophe (name), list of people with this given name or surname * Christophe (singer) (1945–2020), French singer * Cristophe (hairstylist) (born 1958), Belgian hairstylist * Georges Colomb (1856–1945), Frenc ...

in the

OCaml OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...

programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...

. He has continued to lead the current development team, a joint effort of

University of Savoy A university () is an institution of tertiary education and research which awards academic degrees in several academic disciplines. ''University'' is derived from the Latin phrase , which roughly means "community of teachers and scholars". Univ ...

and University Paris VII. The primary aim of the PhoX project creating a user friendly proof checker using the type system developed by

Jean-Louis Krivine Jean-Louis is a given name, especially for French males. Notable people named "Jean-Louis" include: * Jean-Louis Alléon-Dulac, French naturalist * Jean-Louis Aubert, French singer-songwriter, guitarist, composer and producer * Jean-Louis Baribe ...

at University Paris VII. It is meant to be more intuitive than other systems while remaining extensible, efficient, and expressive. Compared to other systems, the proof-building syntax is simplified and closer to natural language. Other features include GUI-driven proof construction, rendering formatted output, and

proof of correctness In theoretical computer science, an algorithm is correct with respect to a specification if it behaves as specified. Best explored is ''functional'' correctness, which refers to the input–output behavior of the algorithm: for each input it prod ...

of programs in the ML programming language. PhoX is currently used to teach logic at Savoy University. It is in an experimental but usable state. It is released under

CeCILL CeCILL (from CEA CNRS INRIA Logiciel Libre) is a free software license adapted to both international and French legal matters, in the spirit of and retaining compatibility with the GNU General Public License (GPL). It was jointly developed by ...

2.0.

External links

Phox website
{{logic-stub Free theorem provers Proof assistants