UNBSynopsisMembersProjectsOnline TPLinks

© Copyrights


P r o j e c t s

This is not the summation of all projects currently ongoing at the UNB Automated Reasoning group. It is the summation of all projects that were documented and the author of this web page was aware of at the time of writing or maintenance.


The most recent research has surrounded clause trees and binary resolution trees, pointedly taking into account their applications and usage with automated theorem provers. The focuses have involved:

  • building minimal proof trees
  • eliminating redundant proof trees
  • iterative deepening techniques
  • disjunctive deductive databases
  • resolution implementation resource management

 Papers and Publications



Bruce Spencer  The Design of j-DREW: A Deductive Reasoning Engine for the Web.This paper was presented at the CologNET workshop held at the LOPSTR conference in Madrid, Spain http://clip.dia.fi.upm.es/SAS-LOPSTR-AGP/schedule-lopstr.html.
PDF file containing the paper.

PPT file containing the presentation.




Bruce Spencer and J. D. Horton, Support Ordered Resolution This paper from CADE-00 in Pittsburg, shows that the rank-activity restriction of binary resolution, described in 1998, can be implemented within a theorem prover based on ordered resolution. Ordered resolution is among the most effective restrictions of resolution, but it can eliminate all small binary resolution trees, leaving only exponentially larger ones. By loosening the ordered restriction with only a very restrictive additional possible inference, we often re-admit these small proofs. Experimental results show a great speed-up in many cases, and very small slow-down in other cases.
Postscript gzip PDF

J.D. Horton and Bruce Spencer, Efficient algorithms to detect and restore minimality: an extension of the regular restriction of resolution This paper extends and revises a published AAAI-97 paper (below), and has been published in Journal of Automated Reasoning, July 2000. It introduces splay surgery, a means of restoring minimality to a binary resolution tree. It also defines support and visibilty in a binary resolution tree, as well as describing a close correspondence between BRTs and Clause Trees (see Clause Trees, 1997).
Postscript gzip PDF


Peter Baumgartner, J.D. Horton and Bruce Spencer, Merge Path Improvements for Minimal Model Hypertableaux Proceedings of Tableaux 99, Albany, New York, pages 51-65, Springer-Verlag LNAI 1617, June 8, 1999. Addresses issues of refutational first-order theorem proving within the clause tree framework with techniques for minimal model computation developed within the hypertableau framework.
Postscript gzip PDF


J. D. Horton and Bruce Spencer, Rank/Activity: A Canonical Form for Binary Resolution: This 15 page paper appeared at CADE in Lindau, July, 1998. It describes the large class of binary resolution proofs that differ only by re-ordering the resolution steps, and an inference-local restriction that admits only one proof in this class.
Postscript gzip PDF


Bruce Spencer and J. D. Horton, Extending the Regular Restruction of Resolution to Non-Linear Subdeductions: This appeared at AAAI-97. This 6 page paper describes a linear time algorithm to decide if some reorderings of resolution steps will render a binary resolution proof tree irregular.
Postscript gzip PDF

J. D. Horton and Bruce Spencer, Clause Trees: A Tool for Understanding and Implementing Resolution in Automated Reasoning: This is the most up-to-date version of Technical Report TR95-095, Computer Science, University of New Brunswick. It appeared in Artificial Intelligence Journal, vol 92. This 74 page paper introduces clause trees, a new methodology/data structure for implementing resolution. It is slighltly fewer pages in AIJ, but otherwise identical.
PostScript gzip PDF


Charlie Obimbo and Bruce Spencer, Using ACTS in Disjunctive Deductive Databases: This paper appeared in the Non-Monotonic Extensions of Logic Programming workshop in Bonn, in conjunction with the JICSLP, 1996.


J. D. Horton and Bruce Spencer, A Top Down Algorithm to Find Only Minimal Clause Trees: In proceedings of CPL-95, held in conjunction with KI-95, Bielefeld, Germany, Sept 1995. This two page paper describes propositional MinALPOC, a top down algorithm for minimal clause trees.
Postscript gzip


Bruce Spencer, Avoiding Duplicate Proofs with the Foothold Refinement: Although this is not strictly a clause tree paper, the data structure described here provided the basis of the clause tree, and the foothold refinement was eventually applied directly to clause trees. The foothold refinement forces the paths that represent ancestor resolution to go in one specific direction. This paper appeared in the Annals of Mathematics and Artificial Intelligence.
Postscript gzip PDF

Bruce Spencer, J.D. Horton and Kelsey Francis, Experiments with ALPOC Theorem Prover: Technical Report TR95-094, Computer Science, University of New Brunswick. This 16 page paper describes a system for automatically running a suite of tests, and the results of running those tests with the ALPOC theorem prover, on a number of problems from the TPTP library.



AllPaths automated theorem prover
PROLOG implementation of a top down algorithm.

AllPaths++ automated theorem prover
Iteration of AllPaths. Although never implemented, it serves as a theoretical advancement over the initial version.

MARMOSET automated theorem prover
OO C++ of bottom up design. Initial localized attempt at instantiating Minimality techniques as well as Surgery.  


Written and maintained by Brian Hunt
Last Modified: