# Mark E. Stickel

According to our database

^{1}, Mark E. Stickel## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### On csauthors.net:

## Bibliography

2009

Building Theorem Provers.

Proceedings of the Automated Deduction, 2009

2004

Deductive Question Answering from Multiple Resources.

Proceedings of the New Directions in Question Answering, 2004

2001

Balance and Filtering in Structured Satisfiable Problems (Preliminary Report).

Electronic Notes in Discrete Mathematics, 2001

Balance and Filtering in Structured Satisfiable Problems.

Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001

2000

Implementing the Davis-Putnam Method.

J. Autom. Reasoning, 2000

Using Prior Knowledge: Problems and Solutions.

Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30, 2000

1997

FASTUS: A Cascaded Finite-State Transducer for Extracting Information from Natural-Language Text

CoRR, 1997

A Practical Integration of First-Order Reasoning and Decision Procedures.

Proceedings of the Automated Deduction, 1997

1995

Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results.

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

Term Rewriting in Contemporary Resolution Theorem Proving (Abstract).

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

1994

Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction.

J. Autom. Reasoning, 1994

Elimination of inference channels by optimal upgrading.

Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, 1994

Ordered Binary Decision Diagrams and the Davis-Putnam Procedure.

Proceedings of the Constraints in Computational Logics, First International Conference, 1994

Deductive Composition of Astronomical Software from Subroutine Libraries.

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

Automated theorem-proving research in the Fifth Generation Computer Systems Project: Model generation theorem provers.

Future Generation Comp. Syst., 1993

Interpretation as Abduction.

Artif. Intell., 1993

Detection and elimination of inference channels in multilevel relational database systems.

Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy, 1993

1992

A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog.

Theor. Comput. Sci., 1992

Proving Properties of Rule-Based Systems.

International Journal of Software Engineering and Knowledge Engineering, 1992

Toward a Tool to Detect and Eliminate Inference Problems in the Design of Multilevel Databases.

Proceedings of the Database Security, 1992

Caching and Lemmaizing in Model Elimination Theorem Provers.

Proceedings of the Automated Deduction, 1992

1991

A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation.

Ann. Math. Artif. Intell., 1991

Abductive and Approximate Reasoning Models for Characterizing Inference Channels.

Proceedings of the 4th IEEE Computer Security Foundations Workshop, 1991

PTTP and Linked Inference.

Proceedings of the Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991

1990

A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog.

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1990

A Prolog Technology Theorem Prover.

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

More Advanced and Powerful Proof Tools.

IFIP Congress, 1989

Rationale and Methods for Abductice Reasoning in Natural-Language Interpretation.

Proceedings of the Natural Language and Logic, 1989

1988

A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler.

J. Autom. Reasoning, 1988

Opening the AC-Unification Race.

J. Autom. Reasoning, 1988

A Prolog Technology Theorem Prover.

Proceedings of the 9th International Conference on Automated Deduction, 1988

The KLAUS Automated Deduction System.

Proceedings of the 9th International Conference on Automated Deduction, 1988

Interpretation as Abduction.

Proceedings of the 26th Annual Meeting of the Association for Computational Linguistics, 1988

1987

A Comparison of the Variable-Abstraction and Constant-Abstraction Methods for Associative-Commutative Unification.

J. Autom. Reasoning, 1987

1986

Schubert's Steamroller Problem: Formulation and Solutions.

J. Autom. Reasoning, 1986

Set Theory in First-Order Logic: Clauses for Gödel's Axioms.

J. Autom. Reasoning, 1986

The KLAUS Automated Deduction System.

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler.

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1985

Automated Deduction by Theory Resolution.

J. Autom. Reasoning, 1985

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

Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, 1985

Automated Deduction by Theory Resolution.

Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, 1985

An Introduction to Automated Deduction.

Proceedings of the Fundamentals of Artificial Intelligence: An Advanced Course, 1985

1984

A Prolog Technology Theorem Prover.

New Generation Comput., 1984

A Prolog Technology Theorem Prover.

Proceedings of the 1984 International Symposium on Logic Programming, 1984

A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity.

Proceedings of the 7th International Conference on Automated Deduction, 1984

1983

A note on leftmost innermost term reduction.

ACM SIGSAM Bulletin, 1983

Theory Resolution: Building in Nonequational Theories.

Proceedings of the National Conference on Artificial Intelligence. Washington, 1983

1982

A Nonclausal Connection-Graph Resolution Theorem-Proving Program.

Proceedings of the National Conference on Artificial Intelligence. Pittsburgh, 1982

1981

A Unification Algorithm for Associative-Commutative Functions.

J. ACM, 1981

Complete Sets of Reductions for Some Equational Theories.

J. ACM, 1981

1976

A Hole in Goal Trees: Some Guidance from Resolution Theory.

IEEE Trans. Computers, 1976

1975

A Complete Unification Algorithm for Associative-Commutative Functions.

Proceedings of the Advance Papers of the Fourth International Joint Conference on Artificial Intelligence, 1975

1973

A Hole in Goal Trees: Some Guidance from Resolution Theory.

Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, 1973