|
|
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
|
2002
|
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.
|
|
2001
|
|
|
2000
|
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
|
|
1999
|
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
|
|
1998
|
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
|
|
1997
|
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
|
|
1996
|
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.
|
|
1995
|
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
|
|
1994
|
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.
|
