Location

Research concerning automated reasoning reflected in these pages is conducted at the University of New Brunswick under the Faculty of Computer Science in Fredericton, New Brunswick, Canada.

We can be reached at the following address:

Faculty of Computer Science
University of New Brunswick
P.O. Box 4400
Fredericton, NB
E3B 5A3

Phone: (506) 453-4566
Fax: (506) 453-3566

Automated what?

Automated Reasoning is somewhat of a misnomer. A more accurate description of our activities would be Automated Argumentation, which corresponds to deductive reasoning, whereas automated reasoning implies induction as well as deduction. On the other hand, automated argumentation is encompassed in automated reasoning (just as argumentation is encompassed in reasoning), and we name our research under the more general and traditional term. An accepted alias for Automated Theorem Proving is automated reasoning whereas automated argumentation is not; calling our research automated reasoning increases its chance of being found by those seeking via internet search engines.

Argumentation and reasoning, as used interchangably, refer to the same thing within these pages, unless explicitly stated otherwise, first order logic. We shall also state automated theorem prover (ATP), the generation mechanism of a theroem proof or model, interchangably with automated argumentation and automated reasoning. For all intents and purposes herein, they are essentially referencing the same principles: automation of logical reasoning for the purpose of theorem proving.

Ethics

Theorems differ from problems in that an ATP can solve a theorem, but very rarely a problem, indicating the difference between automated reasoning/argumentation and artificial intelligence. Problems are solved, theorems are proven. Unlike artificial intelligence, there are no direct non-political ethical issues surrounding the generation and usage of an automated theorem prover.

Without the ability to solve problems, an automated theorem prover is a finite state automaton; it will not induce solutions to external problem sets. Only indirect consequences arising from such research will have ethically questionable outcomes. The presence of a sufficiently robust automated reasoning theoretical foundation is necessary prior to the generation of a reasonably expressive artificial intelligence to pose any ethical quirks. We are a long way off. We all do our own part.

Mechanics

ATP is by definition, the automated (or mechanical without the need of human intervention) generation of a proof of contradiction, or a model indicating that no such proof of contradiction can exist. This is accomplished with propositionally sound multi-level algorithms implemented on a Turing machine (computer). Multi-level algorithms is stated in such a way to reflect the robustness of design sufficient to solve literally complex (ie. non-propositional) problems.

There are many diverse aspects of ATP, and suggested readings include the Journal of Automated Reasoning, Artificial Intelligence, Journal of Logic and Computation, and excerpts among the various conference reports, lecture notes, and proceedings, such as the International Conference on Automated Deduction, International Symposium on Artificial Intelligence and Mathematic, CADE Workshops, IEEE Symposium on Logic in Computer Science, and various technical reports from Argonne National Laboratory.

Motivations

These pages exist to disseminate into the scientific community the results of this research. Also of relevence are the links to people of similar interests, and common goals. Also of note is the existence of an online theorem proving system, onlinetp. This is under generation, and it is hoped that several competent first order logic automated theorem provers will be usable with this system. In the beginning, only the MARMOSET ATP will be available.

Research at the University of New Brunswick in this area directly reflects the demands and constraints laid upon modern theorem provers, in terms of theoretical maxims, and in terms of implementation constraints. Beyond the theoretical research, practical efforts are being made to reflect the growing complexity of computers, their growing raw processing power, and the capabilities offered to this field in economically viable parallel processing and clustering projects.