1. G. M. Adelson-Velskii and E. M. Landis. An algorithm for the organizaton of information.Soviet Math. Doklady, 3:1259–1263, 1962.

   Google Scholar 

2. Chin-Liang Chang and Richard Char-Tung Lee.Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York and London, 1973.

   Google Scholar 

3. Hans de Nivelle. Resolution games and non-liftable resolution orderings.Collegium Logicum, Annals of the Kurt Gödel Society, 2:1–20, 1996.

   MATH  Google Scholar 

4. J. D. Horton and Bruce Spencer. Bottom up procedures to construct each minimal clause tree once. Technical Report TR97-115, Faculty of Computer Science, University of New Brunwsick, PO Box 4400, Fredericton, New Brunswick, Canada, 1997.

   Google Scholar 

5. J. D. Horton and Bruce Spencer. Clause trees: a tool for understanding and implementing resolution in automated reasoning.Artificial Intelligence, 92:25–89, 1997.

   Article MathSciNet  Google Scholar 

6. J. A. Robinson. A machine-oriented logic based on the resolution principle.J. ACM, 12:23–41, 1965.

   Article MATH  Google Scholar 

7. Bruce Spencer and J.D. Horton. Extending the regular restriction of resolution to non-linear subdeductions. InProceedings of the Fourteenth National Conference on Artificial Intelligence, pages 478–483. AAAI Press/MIT Press, 1997.

   Google Scholar 

8. Bruce Spencer and J.D. Horton. Efficient procedures to detect and restore minimality, an extension of the regular restriction of resolution.Journal of Automated Reasoning, 1998. accepted for publication.

   Google Scholar 

9. G. S. Tseitin. On the complexity of derivation in propositional calculus. InStudies in Constructive Mathematics, Seminars in Mathematics: Mathematicheskii Institute, pages 115–125. Consultants Bureau, 1969.

   Google Scholar 

10. L. Wos.Automated Reasoning: 33 Basic Research Problems. Prentice-Hall, Englewood Cliffs, New Jersey, 1988.

    Google Scholar 

Download references