BDBComp
Parceria:
SBC
Implementing a Multi-Strategy Theorem Prover

Adolfo Gustavo Serra Seca NetoMarcelo Finger

An 0.25µm CMOS Injection Locked 5.6Gb/s Clock and Data Recovery Cell

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.

http://www.lbd.dcc.ufmg.br/colecoes/enia/2005/058.pdf

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: bdbcomp@lbd.dcc.ufmg.br
     Mantida por:
LBD