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.