The PhoX Proof Assistant. PhoX is a proof assistant based on High Order logic and it is eXtensible. One of the principle of this proof assistant is to be as user friendly as possible and so to need a minimal learning time. The current version is still expirimental but starts to be really usable. It is a good idea to try it and make comments to improve the final version.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Wiedijk, Freek: A synthesis of the procedural and declarative styles of interactive theorem proving (2012)
- Sacerdoti Coen, Claudio: Declarative representation of proof terms (2010)
- Wiedijk, Freek (ed.): The seventeen provers of the world. Foreword by Dana S. Scott.. (2005)
- Raffalli, C.: Getting results from programs extracted from classical proofs (2004)
- Raffalli, Christophe: System ST toward a type system for extraction and proofs of programs (2003)