os slides da palestra que o Freek Wiedijk apresentou aqui no último LSFA, aqui em Natal http://www.cs.ru.nl/~freek/talks/lsfa.pdf está organizado a partir de um grupo de perguntas bastante interessantes:
1. Should the next generation of proof assistants be based on ZFC set theory? 2. Should the next generation of proof assistants have an advanced type system? 3. Should the next generation of proof assistants take partiality seriously? 4. Should the next generation of proof assistants take category theory seriously? 5. Should the next generation of proof assistants be based on a logical framework? 6. Should the next generation of proof assistants have a self-verified kernel? 7. Should the next generation of proof assistants be programmed in itself? 8. Should the next generation of proof assistants be competitive with commercial computer algebra? 9. Should the next generation of proof assistants use a declarative proof style? 10. How should the next generation of proof assistants be arrived at? (alguém gostaria de dizer como responderia alguma delas?) jm _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
