Implementing a Multi-Strategy Theorem Prover

Adolfo Gustavo Serra Seca NetoMarcelo Finger

We describe the implementation of MSTP, a multi-strategy theorem prover based on the KE Tableau System. Strategies are responsible for the control of (nondeterministic) inference rules of automated deduction systems. MSTP is a theorem prover where we can vary the strategy without modifying the core of the implementation. To achieve the goal of constructing a well-designed and efficient multi-strategy theorem prover, we are using a new software development method, aspect orientation, that allows a better modularization of crosscutting concerns such as strategies. MSTP obtained excellent results compared with a similar tableau-based theorem prover.

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato:
     Mantida por: