Theorem roving Software, Based on Method of Positively-Constructed Formulae
Russian Federation · 2011
The language of positively constructed formulae and its calculus are described in this paper. The results o f a software system development for automated theorem proving in the calculus are presented. The im plementation of the algorithms is based o n different techniques for improving system performance and reduction of the amoun t of used memory. A number o f strategies have been implemented as well.