THURSDAY, AUGUST 9
Favio Miranda
Facultad de Ciencia, UNAM
It has been said that the backwards method for constructing a proof, which goes back to what is called analysis in ancient geometry, is a helpful heuristic but its output should not be considered as a correct proof. Instead, after this discovery methodology has succeed, it is mandatory to construct a forward proof. This is a major drawback when the proofs sought after are not purely mathematical but related to formal verification of software programs. We argue against such point of view by discussing a formal notion of backward proof that allows to define interactive proof-search transition systems, and to establish an equivalence between them and several traditional deductive systems. Thus showing that the backward proof construction is a logically valid process, and hence there is no need for forward proofs.