Disseny i implementació d'un sistema de representació gràfica per a un marc argumentatiu recursiu

En aquest treball final de carrera es disseny i s'implementa un sistema de representació gràfica per a un marc argumentatiu recursiu. El compil·lador s'ha realitzat en Java. Primerament es descriu el llenguatge d'entrada i el disseny general del compil·lador. Posteriorment, es descriuen les fases d'anàlisi lèxica, anàlisi sintàctica i la traducció dirigida per la sintaxi i la taula de símbols. Finalment, s'explica la representació gràfica.

An Interactive Theorem Prover for First-Order Dynamic Logic

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.