![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Mark E. Stickel
Person information
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2010 – 2019
- 2013
- [e2]Maria Paola Bonacina, Mark E. Stickel:
Automated Reasoning and Mathematics - Essays in Memory of William W. McCune. Lecture Notes in Computer Science 7788, Springer 2013, ISBN 978-3-642-36674-1 [contents]
2000 – 2009
- 2009
- [c37]Mark E. Stickel:
Building Theorem Provers. CADE 2009: 306-321 - 2004
- [c36]Richard J. Waldinger, Douglas E. Appelt, Jennifer L. Dungan, John Fry, Jerry R. Hobbs, David J. Israel, Peter Jarvis, David L. Martin, Susanne Z. Riehemann, Mark E. Stickel, Mabry Tyson:
Deductive Question Answering from Multiple Resources. New Directions in Question Answering 2004: 253-262 - 2001
- [j19]Henry A. Kautz
, Yongshao Ruan, Dimitris Achlioptas, Carla P. Gomes, Bart Selman, Mark E. Stickel:
Balance and Filtering in Structured Satisfiable Problems (Preliminary Report). Electron. Notes Discret. Math. 9: 2-18 (2001) - [c35]Henry A. Kautz, Yongshao Ruan, Dimitris Achlioptas, Carla P. Gomes, Bart Selman, Mark E. Stickel:
Balance and Filtering in Structured Satisfiable Problems. IJCAI 2001: 351-358 - 2000
- [j18]Hantao Zhang, Mark E. Stickel:
Implementing the Davis-Putnam Method. J. Autom. Reason. 24(1/2): 277-296 (2000) - [c34]Vinay K. Chaudhri, Mark E. Stickel, Jérôme Thoméré, Richard J. Waldinger:
Using Prior Knowledge: Problems and Solutions. AAAI/IAAI 2000: 436-442
1990 – 1999
- 1997
- [c33]Nikolaj S. Bjørner, Mark E. Stickel, Tomás E. Uribe:
A Practical Integration of First-Order Reasoning and Decision Procedures. CADE 1997: 101-115 - [i1]Jerry R. Hobbs, Douglas E. Appelt, John Bear, David J. Israel, Megumi Kameyama, Mark E. Stickel, Mabry Tyson:
FASTUS: A Cascaded Finite-State Transducer for Extracting Information from Natural-Language Text. CoRR cmp-lg/9705013 (1997) - 1996
- [c32]Jerry R. Hobbs, Douglas E. Appelt, John Bear, David J. Israel, Megumi Kameyama, Andrew Kehler, Mark E. Stickel, Mabry Tyson:
SRI's Tipster II Project. TIPSTER 1996: 201-208 - 1995
- [c31]Mark E. Stickel:
Term Rewriting in Contemporary Resolution Theorem Proving (Abstract). RTA 1995: 101 - [c30]Mark E. Stickel, Hantao Zhang:
Studying Quasigroup Identities by Rewriting Techniques: Problems and First Results. RTA 1995: 450-456 - 1994
- [j17]Mark E. Stickel:
Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction. J. Autom. Reason. 13(2): 189-210 (1994) - [c29]Mark E. Stickel, Richard J. Waldinger, Michael R. Lowry, Thomas Pressburger, Ian Underwood:
Deductive Composition of Astronomical Software from Subroutine Libraries. CADE 1994: 341-355 - [c28]Tomás E. Uribe, Mark E. Stickel:
Ordered Binary Decision Diagrams and the Davis-Putnam Procedure. CCL 1994: 34-49 - [c27]Mark E. Stickel:
Elimination of inference channels by optimal upgrading. S&P 1994: 168-174 - 1993
- [j16]Jerry R. Hobbs, Mark E. Stickel, Douglas E. Appelt, Paul A. Martin:
Interpretation as Abduction. Artif. Intell. 63(1-2): 69-142 (1993) - [j15]Mark E. Stickel:
Automated theorem-proving research in the Fifth Generation Computer Systems Project: Model generation theorem provers. Future Gener. Comput. Syst. 9(2): 143-152 (1993) - [c26]Xiaolei Qian, Mark E. Stickel, Peter D. Karp, Teresa F. Lunt, Thomas D. Garvey:
Detection and elimination of inference channels in multilevel relational database systems. S&P 1993: 196-205 - 1992
- [j14]Richard J. Waldinger, Mark E. Stickel:
Proving Properties of Rule-Based Systems. Int. J. Softw. Eng. Knowl. Eng. 2(1): 121-144 (1992) - [j13]Mark E. Stickel:
A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Theor. Comput. Sci. 104(1): 109-128 (1992) - [c25]Owen L. Astrachan, Mark E. Stickel:
Caching and Lemmaizing in Model Elimination Theorem Provers. CADE 1992: 224-238 - [c24]Thomas D. Garvey, Teresa F. Lunt, Xiaolei Qian, Mark E. Stickel:
Toward a Tool to Detect and Eliminate Inference Problems in the Design of Multilevel Databases. DBSec 1992: 149-168 - 1991
- [j12]Mark E. Stickel:
A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation. Ann. Math. Artif. Intell. 4: 89-105 (1991) - [c23]Zohar Manna, Mark E. Stickel, Richard Waldinger:
Monotonicity Properties in Automated Deduction. Artificial and Mathematical Theory of Computation 1991: 261-280 - [c22]Mark E. Stickel:
PTTP and Linked Inference. Automated Reasoning: Essays in Honor of Woody Bledsoe 1991: 283-296 - [c21]Thomas D. Garvey, Teresa F. Lunt, Mark E. Stickel:
Abductive and Approximate Reasoning Models for Characterizing Inference Channels. CSFW 1991: 118-126 - 1990
- [c20]Mark E. Stickel:
A Prolog Technology Theorem Prover. CADE 1990: 673-674 - [c19]Mark E. Stickel:
A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. DISCO 1990: 154-163 - [e1]Mark E. Stickel:
10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings. Lecture Notes in Computer Science 449, Springer 1990, ISBN 3-540-52885-7 [contents]
1980 – 1989
- 1989
- [c18]Mark E. Stickel:
Rationale and Methods for Abductice Reasoning in Natural-Language Interpretation. Natural Language and Logic 1989: 233-252 - [c17]Mark E. Stickel:
More Advanced and Powerful Proof Tools. IFIP Congress 1989: 791-792 - [c16]Jerry R. Hobbs, Douglas E. Appelt, John Bear, Mark E. Stickel, Mabry Tyson:
TACITUS: A Message Understanding System. HLT (2) 1989 - 1988
- [j11]Mark E. Stickel:
A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. J. Autom. Reason. 4(4): 353-380 (1988) - [j10]Hans-Jürgen Bürckert, Alexander Herold, Deepak Kapur, Jörg H. Siekmann, Mark E. Stickel, Michael Tepp, Hantao Zhang:
Opening the AC-Unification Race. J. Autom. Reason. 4(4): 465-474 (1988) - [c15]Jerry R. Hobbs, Mark E. Stickel, Paul A. Martin, Douglas Edwards:
Interpretation as Abduction. ACL 1988: 95-103 - [c14]Mark E. Stickel:
The KLAUS Automated Deduction System. CADE 1988: 750-751 - [c13]Mark E. Stickel:
A Prolog Technology Theorem Prover. CADE 1988: 752-753 - 1987
- [j9]Mark E. Stickel:
A Comparison of the Variable-Abstraction and Constant-Abstraction Methods for Associative-Commutative Unification. J. Autom. Reason. 3(3): 285-289 (1987) - 1986
- [j8]Mark E. Stickel:
Schubert's Steamroller Problem: Formulation and Solutions. J. Autom. Reason. 2(1): 89-101 (1986) - [j7]Robert S. Boyer, Ewing L. Lusk, William McCune, Ross A. Overbeek, Mark E. Stickel, Larry Wos:
Set Theory in First-Order Logic: Clauses for Gödel's Axioms. J. Autom. Reason. 2(3): 287-327 (1986) - [c12]Mark E. Stickel:
A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. CADE 1986: 573-587 - [c11]Mark E. Stickel:
The KLAUS Automated Deduction System. CADE 1986: 703-704 - 1985
- [j6]Mark E. Stickel:
Automated Deduction by Theory Resolution. J. Autom. Reason. 1(4): 333-355 (1985) - [c10]Mark E. Stickel:
An Introduction to Automated Deduction. Advanced Course: Fundamentals of Artificial Intelligence 1985: 75-132 - [c9]Mark E. Stickel, Mabry Tyson:
An Analysis of Consecutively Bounded Depth-First Search with Applications in Automated Deduction. IJCAI 1985: 1073-1075 - [c8]Mark E. Stickel:
Automated Deduction by Theory Resolution. IJCAI 1985: 1181-1186 - 1984
- [j5]Mark E. Stickel:
A Prolog Technology Theorem Prover. New Gener. Comput. 2(4): 371-383 (1984) - [c7]Mark E. Stickel:
A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity. CADE 1984: 248-258 - [c6]Mark E. Stickel:
A Prolog Technology Theorem Prover. SLP 1984: 211-217 - 1983
- [j4]Mark E. Stickel:
A note on leftmost innermost term reduction. SIGSAM Bull. 17(3-4): 19-20 (1983) - [c5]Mark E. Stickel:
Theory Resolution: Building in Nonequational Theories. AAAI 1983: 391-397 - 1982
- [c4]Mark E. Stickel:
A Nonclausal Connection-Graph Resolution Theorem-Proving Program. AAAI 1982: 229-233 - 1981
- [j3]Gerald E. Peterson, Mark E. Stickel:
Complete Sets of Reductions for Some Equational Theories. J. ACM 28(2): 233-264 (1981) - [j2]Mark E. Stickel:
A Unification Algorithm for Associative-Commutative Functions. J. ACM 28(3): 423-434 (1981)
1970 – 1979
- 1978
- [c3]Mark E. Stickel:
Fuzzy four-valued logic for inconsistency and uncertainty. MVL 1978: 91-94 - 1976
- [j1]Donald W. Loveland, Mark E. Stickel:
A Hole in Goal Trees: Some Guidance from Resolution Theory. IEEE Trans. Computers 25(4): 335-341 (1976) - 1975
- [c2]Mark E. Stickel:
A Complete Unification Algorithm for Associative-Commutative Functions. IJCAI 1975: 71-76 - 1973
- [c1]Donald W. Loveland, Mark E. Stickel:
A Hole in Goal Trees: Some Guidance from Resolution Theory. IJCAI 1973: 153-161
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-24 22:45 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint