Adolfo Gustavo Serra Seca Neto, Marcelo 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.
http://www.lbd.dcc.ufmg.br/colecoes/enia/2005/058.pdfCaso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web