Title :

Proofs using PhoX and new_command

Abstract :

We'll present a proof of a topological property written in a natural 
language (english here). This proof will then be translated into 
new_command, commands in the proof assistant PhoX which have a syntax 
close to natural language and a restricted vocabulary. We'll present 
some difficulties that can be found while translating natural language 
to new_command.
The new_command given to the proof assistant implies a formula that must 
be proved in order to obtain a new state into the proof. We will so 
study some formulas that the automatic prover of PhoX may have to prove.