Mark E. Stickel

AIJ Journal 1993 Journal Article

Interpretation as abduction

• Jerry R. Hobbs
• Mark E. Stickel
• Douglas E. Appelt
• Paul Martin

Abduction is inference to the best explanation. In the TACITUS project at SRI we have developed an approach to abductive inference, called “weighted abduction”, that has resulted in a significant simplification of how the problem of interpreting texts is conceptualized. The interpretation of a text is the minimal explanation of why the text would be true. More precisely, to interpret a text, one must prove the logical form of the text from what is already mutually known, allowing for coercions, merging redundancies where possible, and making assumptions where necessary. It is shown how such “local pragmatics” problems as reference resolution, the interpretation of compound nominals, the resolution of syntactic ambiguity and metonymy, and schema recognition can be solved in this manner. Moreover, this approach of “interpretation as abduction” can be combined with the older view of “parsing as deduction” to produce an elegant and thorough integration of syntax, semantics, and pragmatics, one that spans the range of linguistic phenomena from phonology to discourse structure. Finally, we discuss means for making the abduction process efficient, possibilities for extending the approach to other pragmatics phenomena, and the semantics of the weights and costs in the abduction scheme.

TCS Journal 1992 Journal Article

A Prolog technology theorem prover: a new exposition and implementation in Prolog

• Mark E. Stickel

A Prolog technology theorem prover (PTTP) is an extension of Prolog that is complete for the full first-order predicate calculus. It differs from Prolog in its use of unification with the occurs check for soundness, depth-first iterative-deepening search instead of unbounded depth-first search to make the search strategy complete, and the model elimination reduction rule that is added to Prolog inferences to make the inference system complete. This paper describes a new Prolog-based implementation of PTTP. It uses three compile-time transformations to translate formulas into Prolog clauses that directly execute, with the support of a few run-time predicates, the model elimination procedure with depth-first iterative-deepening search and unification with the occurs check. Its high performance exceeds that of Prolog-based PTTP interpreters, and it is more concise and readable than the earlier Lisp-based compiler, which makes it superior for expository purposes. Examples of inputs and outputs of the compile-time transformations provide an easy and precise way to explain how PTTP works. This Prolog-based version makes it easier to incorporate PTTP theorem-proving ideas into Prolog programs. Some suggestions are made on extensions to Prolog that could be used to improve PTTP's performance.

IJCAI Conference 1985 Conference Paper

An Analysis of Consecutively Bounded Depth-First Search with Applications in Automated Deduction

• Mark E. Stickel
• W. Mabry Tyson

IJCAI Conference 1985 Conference Paper

Automated Deduction by Theory Resolution

• Mark E. Stickel

AAAI Conference 1983 Conference Paper

Theory Resolution: Building in Nonequational Theories

• Mark E. Stickel

Theory resolution constitutes a set of complete proce-dures for building nonequational theories into a resolution theorem-proving program so that axioms of the theory need never be resolved upon. Total theory resolution uses a deci- sion procedure that is capable of determining inconsistency of any set of clauses using predicates in the theory. Partial theory resolution employs a weaker decision procedure that can determine potential inconsistency of a pair of literals. Applications include the building in of both mathematical and special decision procedures, such as for the taxonomic information furnished by a knowledge representation sys-tem.

AAAI Conference 1982 Conference Paper

A Nonclausal Connection-Graph Resolution Theorem-Proving Program

• Mark E. Stickel

A new theorem-proving program, combining the use of non-clausal resolution and connection graphs, is described. The use of nonclausal resolution as the inference system eliminates some of the redundancy and unreadability of clause-based systems. The use of a connection graph restricts the search space and facilitates graph searching for efficient deduction.