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.pdf

Processando consulta.