Symbolic Logic and Mechanical Theorem Proving, 1st edition

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Symbolic Logic and Mechanical Theorem Proving, 1st edition

Source

Pages: 331

Medium: Textbook Hardcover

Year of Publication: 1997

ISBN:0121703509

Authors

Chin-Liang Chang
Richard Char-Tung Lee

Publisher

Academic Press, Inc. Orlando, FL, USA

Bibliometrics

Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 236

Additional Information:

cited by index terms collaborative colleagues

Tools and Actions:	Review this Book Save this Book to a Binder Display Formats: BibTeX EndNote ACM Ref

CITED BY 237

	F. Lin , F. E. Hunt, LCD-reification: a formal method for developing Prolog programs, ACM SIGSOFT Software Engineering Notes, v.14 n.3, p.249-256, May 1989
	Eliezer L. Lozinskii, A problem-oriented inferential database system, ACM Transactions on Database Systems (TODS), v.11 n.3, p.323-356, Sept. 1986
	Steven J. Zeil, A multi-theory constraint satisfaction system, Proceedings of the 1993 ACM conference on Computer science, p.93-99, February 16-18, 1993, Indianapolis, Indiana, United States
	Blayne Mayfield , Timothy Baird, STP: a simple theorem prover for IBM-PC compatible computers, Proceedings of the 1990 ACM SIGSMALL/PC symposium on Small systems, p.98-105, March 28-30, 1990, Crystal City, Virginia, United States
	Michael Kifer , Eliezer L. Lozinskii, On compile-time query optimization in deductive databases by means of static filtering, ACM Transactions on Database Systems (TODS), v.15 n.3, p.385-426, Sept. 1990
	Dennis de Champeaux, Subproblem finder and instance checker, two cooperating modules for theorem provers, Journal of the ACM (JACM), v.33 n.4, p.633-657, Oct. 1986
	L. J. Henschen, Theorem Proving by Covering Expressions, Journal of the ACM (JACM), v.26 n.3, p.385-400, july 1979
	D. Zhang , D. Nguyen, PREPARE: A Tool for Knowledge Base Verification, IEEE Transactions on Knowledge and Data Engineering, v.6 n.6, p.983-989, December 1994
	P. O'Hearn , Z. Stachniak, Note on theorem proving strategies for resolution counterparts of non-classical logics, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation, p.364-372, July 17-19, 1989, Portland, Oregon, United States
	M. Kifer , J. Wu, A logic for object-oriented logic programming, Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.379-393, March 1989, Philadelphia, Pennsylvania, United States
	S. Hegner, Specification and implementation of programs for updating incomplete information databases, Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.146-158, March 23-25, 1987, San Diego, California, United States
	Wray L. Buntine , Hans-Jürgen Bürckert, On solving equations and disequations, Journal of the ACM (JACM), v.41 n.4, p.591-629, July 1994
	Vincent J. Digricoli, Automatic deduction and equality, Proceedings of the 1979 annual conference, p.240-250, January 1979
	J. P. Gallagher, Tutorial on specialisation of logic programs, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.88-98, June 14-16, 1993, Copenhagen, Denmark
	Catriel Beeri , Moshe Y. Vardi, A Proof Procedure for Data Dependencies, Journal of the ACM (JACM), v.31 n.4, p.718-741, Oct. 1984
	Jack Minker , Alan R. Aronson , Barry E. Jacobs, A Note on Fuzzy Deduction, Journal of the ACM (JACM), v.27 n.4, p.599-603, Oct. 1980
	Jun-Jang Jeng , Betty H. C. Cheng, Specification matching for software reuse: a foundation, ACM SIGSOFT Software Engineering Notes, v.20 n.SI, p.97-105, Aug. 1995
	Tanel Tammet, Using resolution for extending KL-ONE-type languages, Proceedings of the fourth international conference on Information and knowledge management, p.326-332, November 29-December 02, 1995, Baltimore, Maryland, United States
	Tie-Cheng Wang, Z-module reasoning: an equality-oriented proving method with built-in ring axioms, Journal of the ACM (JACM), v.40 n.3, p.558-606, July 1993
	Barry E. Jacobs , Anthony C. Klug , Alan R. Aronson, On interpretations of relational languages and solutions to the implied constraint problem, ACM Transactions on Database Systems (TODS), v.7 n.2, p.291-315, June 1982
	Wen-Tsuen Chen , Ming-Yi Fang, Theorem proving in propositional logic on vector computers using a generalized Davis-Putnam procedure, Proceedings of the 1990 conference on Supercomputing, p.658-665, October 1990, New York, New York, United States
	H. Yokota , H. Itoh, A model and an architecture for a relational knowledge base, ACM SIGARCH Computer Architecture News, v.14 n.2, p.2-9, June 1986
	F. Bry, Logic programming as constructivism: a formalization and its application to databases, Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.34-50, March 1989, Philadelphia, Pennsylvania, United States
	Russell Greiner , Christian Darken , N. Iwan Santoso, Efficient reasoning, ACM Computing Surveys (CSUR), v.33 n.1, p.1-30, March 2001
	Mitchell Wand, Continuation-Based Program Transformation Strategies, Journal of the ACM (JACM), v.27 n.1, p.164-180, Jan. 1980
	D. W. Loveland , C. R. Reddy, Deleting Repeated Goals in the Problem Reduction Format, Journal of the ACM (JACM), v.28 n.4, p.646-661, Oct. 1981
	Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, Journal of the ACM (JACM), v.28 n.3, p.423-434, July 1981
	Zohar Manna , Richard Waldinger, Special relations in automated deduction, Journal of the ACM (JACM), v.33 n.1, p.1-59, Jan. 1986
	William W. McCune , Lawrence J. Henschen, Maintaining state constraints in relational databases: a proof theoretic basis, Journal of the ACM (JACM), v.36 n.1, p.46-68, Jan. 1989
	R. C. T. Lee , S. K. Chang, Structured programming and automatic program synthesis, ACM SIGPLAN Notices, v.9 n.4, p.60-70, April 1974
	Stephen A. Cook, Feasibly constructive proofs and the propositional calculus (Preliminary Version), Proceedings of seventh annual ACM symposium on Theory of computing, p.83-97, May 05-07, 1975, Albuquerque, New Mexico, United States
	D W Loveland, Automated theorem proving: mapping logic into AI, Proceedings of the ACM SIGART international symposium on Methodologies for intelligent systems, p.214-229, October 22-24, 1986, Knoxville, Tennessee, United States
	Anthony S. Wojcik, Formal design verification of digital systems, Proceedings of the 20th conference on Design automation, p.228-234, June 27-29, 1983, Miami Beach, Florida, United States
	M. S. Chandrasekhar , J. P. Privitera , K. W. Conradt, Application of term rewriting techniques to hardware design verification, Proceedings of the 24th ACM/IEEE conference on Design automation, p.277-282, June 28-July 01, 1987, Miami Beach, Florida, United States
	Richard C. T. Lee, Fuzzy Logic and the Resolution Principle, Journal of the ACM (JACM), v.19 n.1, p.109-119, Jan. 1972
	Neil V. Murray , Erik Rosenthal, Inference with path resolution and semantic graphs, Journal of the ACM (JACM), v.34 n.2, p.225-254, April 1987
	Ali Mili, A case for teaching program verification: Its importance in the CS curriculum, ACM SIGCSE Bulletin, v.15 n.1, p.2-6, February 1983
	William H. Joiner, Jr., Resolution Strategies as Decision Procedures, Journal of the ACM (JACM), v.23 n.3, p.398-417, July 1976
	Jieh Hsiang , Michaël Rusinowitch, Proving refutational completeness of theorem-proving strategies: the transfinite semantic tree method, Journal of the ACM (JACM), v.38 n.3, p.558-586, July 1991
	Tomasz Imielinski, Abstraction in query processing, Journal of the ACM (JACM), v.38 n.3, p.533-557, July 1991
	John C. Thompson , Dongpil Shin, Data flow relation processor for knowledge base machine, Proceedings of the 1986 ACM fourteenth annual conference on Computer science, p.83-92, February 1986, Cincinnati, Ohio, United States
	Raymond Reiter, Equality and Domain Closure in First-Order Databases, Journal of the ACM (JACM), v.27 n.2, p.235-249, April 1980
	Levent V. Orman, Knowledge base architecture, Proceedings of the 1990 ACM SIGBDP conference on Trends and directions in expert systems, p.325-336, October 30-November 02, 1990, Orlando, Florida, United States
	Georg Gottlob , Nicola Leone , Francesco Scarcello, The complexity of acyclic conjunctive queries, Journal of the ACM (JACM), v.48 n.3, p.431-498, May 2001
	P. B. Powell , P. Thompson, Natural language and voice output for relational data base systems, Proceedings of the 1978 annual conference, p.585-595, January 1978
	Michael Kifer , Georg Lausen , James Wu, Logical foundations of object-oriented and frame-based languages, Journal of the ACM (JACM), v.42 n.4, p.741-843, July 1995
	Norman Rubin , Malcolm C. Harrison, Another Generalization of Resolution, Journal of the ACM (JACM), v.25 n.3, p.341-351, July 1978
	W. Damm, A Microprogramming Logic, IEEE Transactions on Software Engineering, v.14 n.5, p.559-574, May 1988
	Nicole Bidoit , Richard Hull, Positivism vs minimalism in deductive databases, Proceedings of the fifth ACM SIGACT-SIGMOD symposium on Principles of database systems, p.123-132, March 24-26, 1986, Cambridge, Massachusetts, United States
	Robert Jasper , Mike Brennan , Keith Williamson , Bill Currier , David Zimmerman, Test data generation and feasible path analysis, Proceedings of the 1994 ACM SIGSOFT international symposium on Software testing and analysis, p.95-107, August 17-19, 1994, Seattle, Washington, United States
	Jack Minker, Introduction to logic-based artificial intelligence, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2000
	John R. Fisher , Luu Tran, A visual logic, Proceedings of the 1996 ACM symposium on Applied Computing, p.17-21, February 17-19, 1996, Philadelphia, Pennsylvania, United States
	Suk-Chung Yoon , Il-Yeol Song , E. K. Park, Intelligent query answering in deductive and object-oriented databases, Proceedings of the third international conference on Information and knowledge management, p.244-251, November 29-December 02, 1994, Gaithersburg, Maryland, United States
	Michael Fisher , Clare Dixon , Martin Peim, Clausal temporal resolution, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.12-56, Jan. 2001
	Hiroshi G. Okuno , Ikuo Takeuchi , Nobuyasu Osato , Yasushi Hibino , Kazufumi Watanabe, TAO: A fast interpreter-centered system on LISP machine ELIS, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.140-149, August 06-08, 1984, Austin, Texas, United States
	G. E. Peterson, Theorem Proving with Lemmas, Journal of the ACM (JACM), v.23 n.4, p.573-581, Oct. 1976
	W. Bibel , E. Eder, Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution, Journal of the ACM (JACM), v.44 n.2, p.320-344, March 1997
	R. B. Terwilliger , R. H. Campbell, An early report on encompass, Proceedings of the 10th international conference on Software engineering, p.344-354, April 11-15, 1988, Singapore
	G. Gottlob , A. Leitsch, On the efficiency of subsumption algorithms, Journal of the ACM (JACM), v.32 n.2, p.280-295, April 1985
	S Kundu, Tree resolution and generalized semantic tree, Proceedings of the ACM SIGART international symposium on Methodologies for intelligent systems, p.270-278, October 22-24, 1986, Knoxville, Tennessee, United States
	Richard Rankin , Ralph Wilkerson, Proving functionally difficult problems through model generation, Proceedings of the 1992 ACM/SIGAPP Symposium on Applied computing: technological challenges of the 1990's, p.526-529, April 1992, Kansas City, Missouri, United States
	Chris Merz , Ralph Wilkerson, Experimentation with proof methods for non-Horn sets, Proceedings of the 1992 ACM/SIGAPP Symposium on Applied computing: technological challenges of the 1990's, p.530-535, April 1992, Kansas City, Missouri, United States
	George L. Sicherman , Wiebren De Jonge , Reind P. Van de Riet, Answering queries without revealing secrets, ACM Transactions on Database Systems (TODS), v.8 n.1, p.41-59, March 1983
	Gyula Magó, Data sharing in an FFP machine, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.201-207, August 15-18, 1982, Pittsburgh, Pennsylvania, United States
	Neil D. Jones , William T. Laaser, Complete problems for deterministic polynomial time, Proceedings of the sixth annual ACM symposium on Theory of computing, p.40-46, April 30-May 02, 1974, Seattle, Washington, United States
	Ping Wu , Stanley Y. W. Su, Rule validation based on logical deduction, Proceedings of the second international conference on Information and knowledge management, p.164-173, November 01-05, 1993, Washington, D.C., United States
	Steve Winker , L. Wos, Automated generation of models and counterexamples and its application to open questions in Ternary Boolean algebra, Proceedings of the eighth international symposium on Multiple-valued logic, p.251-256, January 1978, Rosemont, Illinois, United States
	Mohammad R. Haghighat , Constantine D. Polychronopoulos, Symbolic analysis for parallelizing compilers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.4, p.477-518, July 1996
	Véronique Royer, Backward chaining evaluation in stratified disjunctive theories, Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.183-195, April 02-04, 1990, Nashville, Tennessee, United States
	Yasushi Hibino, A practical parallel garbage collection algorithm and its implementation, Proceedings of the 7th annual symposium on Computer Architecture, p.113-120, May 06-08, 1980, La Baule, United States
	Upen S. Chakravarthy , John Grant , Jack Minker, Logic-based approach to semantic query optimization, ACM Transactions on Database Systems (TODS), v.15 n.2, p.162-207, June 1990
	Wolfgang Bibel, Matings in matrices, Communications of the ACM, v.26 n.11, p.844-852, Nov. 1983
	Jack Minker, Performing inferences over relation data bases, Proceedings of the 1975 ACM SIGMOD international conference on Management of data, May 14-16, 1975, San Jose, California
	Raymond Reiter, A sound and sometimes complete query evaluation algorithm for relational databases with null values, Journal of the ACM (JACM), v.33 n.2, p.349-370, April 1986
	LiFeng He , Chao Yuyan , Nakamura Tsuyoshi , Itoh Hidenori, I-SATCHMORE: an improvement of A-SATCHMORE, Journal of Computer Science and Technology, v.18 n.2, p.181-189, March 2003
	Paolo Camurati , Tiziana Margaria , Paolo Prinetto, Resolution-based correctness proofs of synchronous circuits, Proceedings of the conference on European design automation, February 25-28, 1991, Amsterdam, The Netherlands
	Dong-Tsan Lee, Evaluating real-time software specification languages, Computer Standards & Interfaces, v.24 n.5, p.395-409, November 2002
	Akihiro Yamamoto, Hypothesis finding based on upward refinement of residue hypotheses, Theoretical Computer Science, v.298 n.1, p.5-19, 4 April 2003
	Jürgen Dix , Ulrich Furbach , Ilkka Niemelä, Nonmonotonic reasoning: towards efficient calculi and implementations, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Christoph Weidenbach, Combining superposition, sorts and splitting, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	C. T. Yu , W. Sun, Automatic Knowledge Acquisition and Maintenance for Semantic Query Optimization, IEEE Transactions on Knowledge and Data Engineering, v.1 n.3, p.362-375, September 1989
	Yoshihiko Futamura , Zenjiro Konishi , Robert Glück, WSDFU: program transformation system based on generalized partial computation, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
	Donald W. Loveland , Adnan H. Yahya, SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, New Generation Computing, v.21 n.3, p.177-207, March 2003
	David Basin , Alan Bundy , Ina Kraan , Sean Matthews, A framework for program development based on schematic proof, Proceedings of the 7th international workshop on Software specification and design, December 06-07, 1993, Redondo Beach, California
	Yoshihiko Futamura , Zenjiro Konishi , Robert Glück, Program transformation system based on generalized partial computation, New Generation Computing, v.20 n.1, p.75-99, January 2002
	L. Bolo , K. Kochut , A. Leśniewski , T. Strzałkowski, Natural, language information retrieval system dialog, Proceedings of the first conference on European chapter of the Association for Computational Linguistics, p.196-203, September 01-02, 1983, Pisa, Italy
	Xavier Rival, Symbolic transfer function-based approaches to certified compilation, ACM SIGPLAN Notices, v.39 n.1, p.1-13, January 2004
	N. Roussopoulos , N. Economou , A. Stamenas, ADMS: A Testbed for Incremental Access Methods, IEEE Transactions on Knowledge and Data Engineering, v.5 n.5, p.762-774, October 1993
	C. Lin , A. Chaudhury , A. Whinston , D. C. Marinescu, Logical Inference of Horn Clauses in Petri Net Models, IEEE Transactions on Knowledge and Data Engineering, v.5 n.3, p.416-425, June 1993
	G. Di Battista , M. Lenzerini, Deductive Entity Relationship Modeling, IEEE Transactions on Knowledge and Data Engineering, v.5 n.3, p.439-450, June 1993
	S. C. Yoon , I. Y. Song , E. K. Park, Semantic query processing in object-oriented databases using deductive approach, Proceedings of the fourth international conference on Information and knowledge management, p.150-157, November 29-December 02, 1995, Baltimore, Maryland, United States
	Krzysztof R. Apt , M. H. van Emden, Contributions to the Theory of Logic Programming, Journal of the ACM (JACM), v.29 n.3, p.841-862, July 1982
	S. Ceri , G. Gottlob , L. Tanca, What You Always Wanted to Know About Datalog (And Never Dared to Ask), IEEE Transactions on Knowledge and Data Engineering, v.1 n.1, p.146-166, March 1989
	A. Basu, A Knowledge Representation Model for Multiuser Knowledge-Based Systems, IEEE Transactions on Knowledge and Data Engineering, v.5 n.2, p.177-189, April 1993
	John Grant , Barry E. Jacobs, On the family of generalized dependency constraints, Journal of the ACM (JACM), v.29 n.4, p.986-997, Oct. 1982
	Kioumars Yazdanian , Frédéric Cuppens, Neighborhood data and database security, Proceedings on the 1992-1993 workshop on New security paradigms, p.150-154, August 1993, Little Compton, Rhode Island, United States
	Henryk Rybiński, On first-order-logic databases, ACM Transactions on Database Systems (TODS), v.12 n.3, p.325-349, Sept. 1987
	A. Illarramendi , J. M. Blanco , A. Goñi, Making the Knowledge Base Systems More Efficient: A Method to Detect Inconsistent Queries, IEEE Transactions on Knowledge and Data Engineering, v.6 n.4, p.634-639, August 1994
	C. S. Ku , H. D. Kim , L. J. Henschen, An Efficient Indefiniteness Inference Scheme in Indefinite Deductive Databases, IEEE Transactions on Knowledge and Data Engineering, v.6 n.5, p.713-722, October 1994
	Paliath Narendran , Jonathan Stillman, Formal verification of the Sobel image processing chip, Proceedings of the 25th ACM/IEEE conference on Design automation, p.211-217, June 12-15, 1988, Atlantic City, New Jersey, United States
	M. -Y. Fang , W. -T. Chen, Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers, IEEE Transactions on Knowledge and Data Engineering, v.4 n.5, p.475-486, October 1992
	J. M. Nicolas, First order logic formalization for functional, multivalued and mutual dependencies, Proceedings of the 1978 ACM SIGMOD international conference on management of data, May 31-June 02, 1978, Austin, Texas
	Hans de Nivelle , Maarten de Rijke, Deciding the guarded fragments by resolution, Journal of Symbolic Computation, v.35 n.1, p.21-58, January 2003
	M. Baaz , A. Leitsh, A strong problem reduction method based on function introduction, Proceedings of the international symposium on Symbolic and algebraic computation, p.30-37, August 20-24, 1990, Tokyo, Japan
	David A. Plaisted , Adnan Yahya, A relevance restriction strategy for automated deduction, Artificial Intelligence, v.144 n.1-2, p.59-93, March 2003
	Herve Gallaire , Jack Minker , Jean-Marie Nicolas, Logic and Databases: A Deductive Approach, ACM Computing Surveys (CSUR), v.16 n.2, p.153-185, June 1984
	R. Peikert, Automated theorem proving: the resolution method, ACM SIGSAM Bulletin, v.21 n.3, p.61-68, Aug. 1987
	T. J. Weigert , J. J. -P. Tsai, A Computationally Tractable Nonmonotonic Logic, IEEE Transactions on Knowledge and Data Engineering, v.6 n.1, p.57-63, February 1994
	Levent V. Orman, Differential Relational Calculus for Integrity Maintenance, IEEE Transactions on Knowledge and Data Engineering, v.10 n.2, p.328-341, March 1998
	Tadao Murata , Du Zhang, A Predicate-Transition Net Model for Parallel Interpretation of Logic Programs, IEEE Transactions on Software Engineering, v.14 n.4, p.481-497, April 1988
	John Grant, A course in applied logic, ACM SIGCSE Bulletin, v.16 n.3, p.26-28, September 1984
	Hioryuki Yamauchi, Processing of syntax and semantics of natural language by predicate logic, Proceedings of the 8th conference on Computational linguistics, September 30-October 04, 1980, Tokyo, Japan
	Micheal Kifer , Eliezer L. Lozinskii, SYGRAF: Implementing Logic Programs in a Database Style, IEEE Transactions on Software Engineering, v.14 n.7, p.922-935, July 1988
	Stuart C. Shapiro, Representing and locating deduction rules in a semantic network, ACM SIGART Bulletin
	Terje Sivertsen, Undefinedness vs. underspecification in HALDEN ASL, Nordic Journal of Computing, v.11 n.1, p.12-34, Spring 2004
	Gabriela Alexe , Sorin Alexe , Yves Crama , Stephan Foldes , Peter L. Hammer , Bruno Simeone, Consensus algorithms for the generation of all maximal bicliques, Discrete Applied Mathematics, v.145 n.1, p.11-21, 30 December 2004
	Ştefan Andrei, Counting for Satisfiability by Inverting Resolution, Artificial Intelligence Review, v.22 n.4, p.339-366, December 2004
	J. Kljaich, Jr. , B. T. Smith , A. S. Wojcik, Formal Verification of Fault Tolerance Using Theorem-Proving Techniques, IEEE Transactions on Computers, v.38 n.3, p.366-376, March 1989
	Deepak Kapur , Paliath Narendran, An equational approach to theorem proving in first-order predicate calculus, ACM SIGSOFT Software Engineering Notes, v.10 n.4, August 1985
	Kathleen Dahlgren , Joyce McDowell , Edward P. Stabler, Knowledge representation for commonsense reasoning with text, Computational Linguistics, v.15 n.3, p.149-170, September 1989
	Dafa Li, The equality axioms are not independent, ACM SIGACT News, v.35 n.3, p.98-101, September 2004
	James Kilbury, Parsing with Category Coocurrence Restrictions, Proceedings of the 12th conference on Computational linguistics, p.324-327, August 22-27, 1988, Budapest, Hungry
	A. Dutta, Integrating Heuristic Knowledge and Optimization Models for Communication Network Design, IEEE Transactions on Knowledge and Data Engineering, v.5 n.6, p.999-1017, December 1993
	Peter Baumgartner, First-order logic Davis-Putnam-Logemann-Loveland procedure, Exploring artificial intelligence in the new millennium, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
	Xubo Zhang , Z. Meral Ozsoyoglu, Implication and Referential Constraints: A New Formal Reasoning, IEEE Transactions on Knowledge and Data Engineering, v.9 n.6, p.894-910, November 1997
	Ron Sun, Structuring Knowledge In Vague Domains, IEEE Transactions on Knowledge and Data Engineering, v.7 n.1, p.120-136, February 1995
	Robert H. Bourdeau , Betty H. C. Cheng, A Formal Semantics for Object Model Diagrams, IEEE Transactions on Software Engineering, v.21 n.10, p.799-821, October 1995
	Sang Ho Lee , Lawrence J. Henschen, Evaluation of Recursive Queries with Extended Rules in Deductive Databases, IEEE Transactions on Knowledge and Data Engineering, v.7 n.2, p.328-331, April 1995
	Niels H. Christensen , Robert Glück, Offline partial evaluation can be as accurate as online partial evaluation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.1, p.191-220, January 2004
	A. Formica, Finite Satisfiability of Integrity Constraints in Object-Oriented Database Schemas, IEEE Transactions on Knowledge and Data Engineering, v.14 n.1, p.123-139, January 2002
	Marin Vlada, Algorithms for Testing Satisfiability Formulas, Artificial Intelligence Review, v.15 n.3, p.153-163, May 2001
	Mark Johnson, Computing with features as formulae, Computational Linguistics, v.20 n.1, p.1-25, March 1994
	D. Sarkar , S. C. De Sarkar, A Theorem Prover for Verifying Iterative Programs Over Integers, IEEE Transactions on Software Engineering, v.15 n.12, p.1550-1566, December 1989
	Eyal Amir , Sheila McIlraith, Partition-based logical reasoning for first-order and propositional theories, Artificial Intelligence, v.162 n.1-2, p.49-88, February 2005
	Wray Buntine, Will Domain-Specific Code Synthesis Become a Silver Bullet?, IEEE Intelligent Systems, v.13 n.2, p.9-15, March 1998
	Boris Konev , Anatoli Degtyarev , Clare Dixon , Michael Fisher , Ullrich Hustadt, Mechanising first-order temporal resolution, Information and Computation, v.199 n.1-2, p.55-86, 25 May 2005
	Linh Anh Nguyen , Rajeev Goré, Completeness of hyper-resolution via the semantics of disjunctive logic programs, Information Processing Letters, v.95 n.2, p.363-369, 31 July 2005
	Jack Minker, Information storage and retrieval: a survey and functional description, ACM SIGIR Forum, v.12 n.2, p.12-108, Fall 1977
	Chao-Chih Yang, Deduction Graphs: An Algorithm and Applications, IEEE Transactions on Software Engineering, v.15 n.1, p.60-67, January 1989
	D. Sarkar , S. C. De Sarkar, A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers, IEEE Transactions on Software Engineering, v.15 n.11, p.1368-1381, November 1989
	D. Sarkar , S. C. De Sarkar, Some Inference Rules for Integer Arithmetic for Verification of Flowchart Programs on Integers, IEEE Transactions on Software Engineering, v.15 n.1, p.1-9, January 1989
	X. Nie , David A. Plaisted, Experimental Results on Subgoal Reordering, IEEE Transactions on Computers, v.39 n.6, p.845-848, June 1990
	Peter Idestam-Almquist, Generalization of Clauses Relative to a Theory, Machine Learning, v.26 n.2-3, p.213-226, Feb./March 1, 1997
	Ben Wegbreit, Goal-directed program transformation, Proceedings of the 3rd ACM SIGACT-SIGPLAN symposium on Principles on programming languages, p.153-170, January 19-21, 1976, Atlanta, Georgia
	Marcelo Finger , Renata Wassermann, The universe of propositional approximations, Theoretical Computer Science, v.355 n.2, p.153-166, 11 April 2006
	Sven Hartmann , Sebastian Link, Horn clauses and functional dependencies in complex-value databases, Proceedings of the 17th Australasian Database Conference, p.21-30, January 16-19, 2006, Hobart, Australia
	Yulia Korukhova, An approach to automatic deductive synthesis of functional programs, Annals of Mathematics and Artificial Intelligence, v.50 n.3-4, p.255-271, August 2007
	Vincent J. Digricoli , Malcolm C. Harrison, Equality-based binary resolution, Journal of the ACM (JACM), v.33 n.2, p.253-289, April 1986
	Mladen Stanojević , Sanja Vraneš, Knowledge representation with SOUL, Expert Systems with Applications: An International Journal, v.33 n.1, p.122-134, July, 2007
	Linh Anh Nguyen, Negative ordered hyper-resolution as a proof procedure for disjunctive logic programming, Fundamenta Informaticae, v.70 n.4, p.351-366, April 2006
	Stefan Brass , Christian Goldberg, Semantic errors in SQL queries: a quite complete list, Journal of Systems and Software, v.79 n.5, p.630-644, May 2006
	Jun Ma , Wenjiang Li , Da Ruan , Yang Xu, Filter-based resolution principle for lattice-valued propositional logic LP(X), Information Sciences: an International Journal, v.177 n.4, p.1046-1062, February, 2007
	Jeremy Bongio , Cyrus Katrak , Hai Lin , Christopher Lynch , Ralph Eric McGregor, Encoding First Order Proofs in SMT, Electronic Notes in Theoretical Computer Science (ENTCS), v.198 n.2, p.71-84, May, 2008
	Elisa Burato , Matteo Cristani, Contract clause negotiation by game theory, Proceedings of the 11th international conference on Artificial intelligence and law, June 04-08, 2007, Stanford, California
	Naci S. Ishakbeyoglu , Z. Meral Ozsoyoglu, Maintenance of implication integrity constraints under updates to constraints, The VLDB Journal — The International Journal on Very Large Data Bases, v.7 n.2, p.67-78, May 1998
	Benjamin Han , Shie-Jue Lee , Hsin-Tai Yang, A Model-Based Diagnosis System for Identifying Faulty Components in Digital Circuits, Applied Intelligence, v.10 n.1, p.37-52, January 1999
	O. V. German , D. V. Semeryuk, On the Polynomially Solvable Problem of Designing Behavior of the Intelligent Robot, Automation and Remote Control, v.62 n.2, p.181-189, February 2001
	Suning Wang , Peter E. Caines, Automated reasoning with function evaluation for COCOLOG, Annals of Mathematics and Artificial Intelligence, v.20 n.1-4, p.301-334, 1997
	Clare Dixon, Temporal resolution using a breadth-first search, Annals of Mathematics and Artificial Intelligence, v.22 n.1-2, p.87-115, 1998
	Qingxun Yu , Mohammed Almulla , Monroe Newborn, Heuristics used by HERBY for semantic tree theorem proving, Annals of Mathematics and Artificial Intelligence, v.23 n.3-4, p.247-266, 1998
	Marc Fuchs , Matthias Fuchs, Feature‐based learning of search‐guiding heuristics for theorem proving, AI Communications, v.11 n.3,4, p.175-189, December 1998
	François Bry , Rainer Manthey, Checking Consistency of Database Constraints: a Logical Basis, Proceedings of the 12th International Conference on Very Large Data Bases, p.13-20, August 25-28, 1986
	Giuseppe Di Battista , M. Lenzerini, A deductive method for entity-relationship modeling, Proceedings of the 15th international conference on Very large data bases, p.13-21, July 1989, Amsterdam, The Netherlands
	Stefan Böttcher , Matthias Jarke , Joachim W. Schmidt, Adaptive Predicate Managers in Database Systems, Proceedings of the 12th International Conference on Very Large Data Bases, p.21-29, August 25-28, 1986
	Eliezer L. Lozinskii, Computing Facts in Non-Horn Deductive Systems, Proceedings of the 14th International Conference on Very Large Data Bases, p.273-279, August 29-September 01, 1988
	Robert B. Terwilliger, Please: a language combining imperative and logic programming, ACM SIGPLAN Notices, v.23 n.4, p.103-110, April, 1988
	Vijay Chandru , Suman Roy , Ramesh Subrahmanyam, Negation as Failure as Resolution, Constraints, v.3 n.4, p.315-329, October 1998
	A. D. Zakrevskii, Logical Equations with Applications to Automatic Design and Control, Automation and Remote Control, v.65 n.4, p.660-670, April 2004
	Irina Rish , Rina Dechter, Resolution versus Search: Two Strategies for SAT, Journal of Automated Reasoning, v.24 n.1-2, p.225-275, February 2000
	John Grant , Jack Minker, A logic-based approach to data integration, Theory and Practice of Logic Programming, v.2 n.3, p.323-368, May 2002
	Chih-Hung Wu , Shie-Jue Lee, Parallelization of a Hyper-Linking–Based Theorem Prover, Journal of Automated Reasoning, v.26 n.1, p.67-106, January 2001
	G. A. Ringwood, SLD: a folk acronym?, ACM SIGPLAN Notices, v.24 n.5, p.71-75, May 1989
	Guilherme Bittencourt , Isabel Tonin, An Algorithm for Dual Transformation in First-Order Logic, Journal of Automated Reasoning, v.27 n.4, p.353-389, November 2001
	Jürgen Avenhaus , David A. Plaisted, General Algorithms for Permutations in Equational Inference, Journal of Automated Reasoning, v.26 n.3, p.223-268, April 2001
	Hans De Nivelle, An Algorithm for the Retrieval of Unifiers from Discrimination Trees, Journal of Automated Reasoning, v.20 n.1-2, p.5-25, April 1998
	Anatoli Degtyarev , Andrei Voronkov, What You Always Wanted to Know about Rigid E-Unification, Journal of Automated Reasoning, v.20 n.1-2, p.47-80, April 1998
	Jinzhao Wu , Zhuojun Liu, Well-Behaved Inference Rules for First-Order Theorem Proving, Journal of Automated Reasoning, v.21 n.3, p.381-400, December 1998
	Bruce Spencer , J. D. Horton, Efficient Algorithms to Detect and Restore Minimality, an Extension of the Regular Restriction of Resolution, Journal of Automated Reasoning, v.25 n.1, p.1-34, July 2000
	Reinhold Letz, LINUS - A Link Instantion Prover with Unit Support, Journal of Automated Reasoning, v.18 n.2, p.205-210, April 1997
	M. Paramasivam , David A. Plaisted, RRTP - A Replacement Rule Theorem Prover, Journal of Automated Reasoning, v.18 n.2, p.221-226, April 1997
	Li Dafa, Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving, Journal of Automated Reasoning, v.18 n.1, p.105-134, February 1997
	O. L. Astrachan , D. W. Loveland, The Use of Lemmas in the Model Elimination Procedure, Journal of Automated Reasoning, v.19 n.1, p.117-141, August 1997
	David Sturgill , Alberto Maria Segre, Nagging: A Distributed, Adversarial Search-Pruning Technique Applied to First-Order Inference, Journal of Automated Reasoning, v.19 n.3, p.347-376, December 1997
	David A. Plaisted , Yunshan Zhu, Ordered Semantic Hyper-Linking, Journal of Automated Reasoning, v.25 n.3, p.167-217, October 2000
	Andrea Formisano , Alberto Policriti, T-Resolution: Refinements and Model Elimination, Journal of Automated Reasoning, v.22 n.4, p.433-483, May 1999
	Peter Baumgartner , Stefan Brüning, A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion, Journal of Automated Reasoning, v.19 n.2, p.205-262, October 1997
	John H. Reif , Simon Kasif , Deepak Sherlekar, Formula dissection: A parallel algorithm for constraint satisfaction, Computers & Mathematics with Applications, v.55 n.6, p.1170-1177, March, 2008
	Peter Baumgartner , Cesare Tinelli, The model evolution calculus as a first-order DPLL method, Artificial Intelligence, v.172 n.4-5, p.591-632, March, 2008
	Youssef Hanna, SLEDE: lightweight verification of sensor network security protocol implementations, The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers, September 03-07, 2007, Dubrovnik, Croatia
	Youssef Hanna, SLEDE: lightweight verification of sensor network security protocol implementations, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
	Alessandro Armando , Maria Paola Bonacina , Silvio Ranise , Stephan Schulz, New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic (TOCL), v.10 n.1, p.1-51, January 2009
	Fatiha Saïs , Nathalie Pernelle , Marie-Christine Rousset, L2R: a logical method for reference reconciliation, Proceedings of the 22nd national conference on Artificial intelligence, p.329-334, July 22-26, 2007, Vancouver, British Columbia, Canada
	Yu-Yan Chao , Li-Feng He , Tsuyoshi Nakamura , Zheng-Hao Shi , Kenji Suzuki , Hidenori Itoh, An Improvement of Herbrand's theorem and its application to model generation theorem proving, Journal of Computer Science and Technology, v.22 n.4, p.541-553, July 2007
	Xiang Li , Baoding Liu, Foundation of credibilistic logic, Fuzzy Optimization and Decision Making, v.8 n.1, p.91-102, March 2009
	Bill MacCartney , Sheila McIlraith , Eyal Amir , Tomás E. Uribe, Practical partition-based theorem proving for large knowledge bases, Proceedings of the 18th international joint conference on Artificial intelligence, p.89-96, August 09-15, 2003, Acapulco, Mexico
	Peter Idestam-Almquist, Generalization of clauses under implication, Journal of Artificial Intelligence Research, v.3 n.1, p.467-489, June 1995
	Philippe Adjiman , Philippe Chatalic , François Goasdoué , Marie-Christine Rousset , Laurent Simon, Distributed reasoning in a peer-to-peer setting: application to the semantic web, Journal of Artificial Intelligence Research, v.25 n.1, p.269-314, January 2006
	Setsuo Ohsuga, Predicate logic involving data structure as a knowledge representation language, Proceedings of the Eighth international joint conference on Artificial intelligence, p.391-394, August 08-12, 1983, Karlsruhe, West Germany
	Alan Bundy, Discovery and reasoning in mathematics, Proceedings of the 9th international joint conference on Artificial intelligence, p.1221-1230, August 18-23, 1985, Los Angeles, California
	Chuck Rieger , Handy Trigg , Bob Bane, ZMOB: a new computing engine for AI, Proceedings of the 7th international joint conference on Artificial intelligence, p.955-960, August 24-28, 1981, Vancouver, BC, Canada
	Dan Benanav, Recognizing unnecessary inference, Proceedings of the 11th international joint conference on Artificial intelligence, p.366-371, August 20-25, 1989, Detroit, Michigan
	Norbert Fisinger, Subsumption and connection graphs, Proceedings of the 7th international joint conference on Artificial intelligence, p.480-486, August 24-28, 1981, Vancouver, BC, Canada
	Rolf Socher-Ambrosius, Reducing the derivation of redundant clauses in reasoning systems, Proceedings of the 11th international joint conference on Artificial intelligence, p.401-406, August 20-25, 1989, Detroit, Michigan
	Younghwan Lim , Lawrence J. Henschen, A new hyperparamodulation strategy for the equality relation, Proceedings of the 9th international joint conference on Artificial intelligence, p.1138-1145, August 18-23, 1985, Los Angeles, California
	Deepak Kapur , Paliath Narendran, An equational approach to theorem proving in first-order predicate calculus, Proceedings of the 9th international joint conference on Artificial intelligence, p.1146-1153, August 18-23, 1985, Los Angeles, California
	Shan-Hwei Nienhuys-Cheng , Ronald de Wolf, Least generalizations and greatest specializations of sets of clauses, Journal of Artificial Intelligence Research, v.4 n.1, p.341-363, Jnauary 1996
	Neil V. Murray , Erik Rosenthal, Path resolution with link deletion, Proceedings of the 9th international joint conference on Artificial intelligence, p.1187-1193, August 18-23, 1985, Los Angeles, California
	Liu XuHua, Lock, linear κ-paramodulation in operator fuzzy logic, Proceedings of the 11th international joint conference on Artificial intelligence, p.435-440, August 20-25, 1989, Detroit, Michigan
	Eyal Amir , Allen Chang, Learning partially observable deterministic action models, Journal of Artificial Intelligence Research, v.33 n.1, p.349-402, September 2008
	Herve Gallaire , Claudine Lasserre, Controlling knowledge deduction in a declarative approach, Proceedings of the 6th international joint conference on Artificial intelligence, p.1-6, August 20-23, 1979, Tokyo, Japan
	Thomas B. Kane, Maximum entropy in Nilsson's probabilistic logic, Proceedings of the 11th international joint conference on Artificial intelligence, p.452-457, August 20-25, 1989, Detroit, Michigan
	Makoto Nagao , Jun-ichi Tsujii , Katsuto Nakajima , Kei Mitamura , Hachidai Ito, LISP machine NK3 and measurement of its performance, Proceedings of the 6th international joint conference on Artificial intelligence, p.625-627, August 20-23, 1979, Tokyo, Japan
	John Slaney, SCOTT: a model-guided theorem prover, Proceedings of the 13th international joint conference on Artifical intelligence, p.109-114, August 28-September 03, 1993, Chambery, France
	William A. Kornfeld, Equality for prolog, Proceedings of the Eighth international joint conference on Artificial intelligence, p.514-519, August 08-12, 1983, Karlsruhe, West Germany
	Setsuo Ohsuga, Theoretical basis for a knowledge representation system, Proceedings of the 6th international joint conference on Artificial intelligence, p.676-683, August 20-23, 1979, Tokyo, Japan
	Paul Fodor, Existentially quantified values for queries and updates of facts in transaction logic programs, Proceedings of the 23rd national conference on Artificial intelligence, p.1798-1799, July 13-17, 2008, Chicago, Illinois
	Antoni Ligeza, A note on backward dual resolution and its application to proving completeness of rule-based systems, Proceedings of the 13th international joint conference on Artifical intelligence, p.132-137, August 28-September 03, 1993, Chambery, France
	David Poole, Average-case analysis of a search algorithm for estimating prior and posterior probabilities in Bayesian networks with extreme probabilities, Proceedings of the 13th international joint conference on Artifical intelligence, p.606-612, August 28-September 03, 1993, Chambery, France
	Richard C. T. Lee, Fuzzy logic and the resolution principle, Proceedings of the 2nd international joint conference on Artificial intelligence, p.560-567, September 01-03, 1971, London, England
	Donald P. MoKay , Stuart C. Shapiro, Using active connection graphs for reasoning with recursive rules, Proceedings of the 7th international joint conference on Artificial intelligence, p.368-374, August 24-28, 1981, Vancouver, BC, Canada
	Masamichi Shimura, Resolution in a new modal logic, Proceedings of the 6th international joint conference on Artificial intelligence, p.809-814, August 20-23, 1979, Tokyo, Japan
	Eliezer L. Lozinskii, Evaluating queries in deductive databases by generating, Proceedings of the 9th international joint conference on Artificial intelligence, p.173-177, August 18-23, 1985, Los Angeles, California
	David A. Plaisted , Yunshan Zhu, Equational reasoning using AC constraints, Proceedings of the 15th international joint conference on Artifical intelligence, p.108-113, August 23-29, 1997, Nagoya, Japan
	David Poole, Variables in hypotheses, Proceedings of the 10th international joint conference on Artificial intelligence, p.905-908, August 23-28, 1987, Milan, Italy
	W. W. Bledsoe, Set variables, Proceedings of the 5th international joint conference on Artificial intelligence, p.501-510, August 22-25, 1977, Cambridge, USA
	Sharon Sickel, Formal grammars as models of logic derivations, Proceedings of the 5th international joint conference on Artificial intelligence, p.544-551, August 22-25, 1977, Cambridge, USA
	Didier Dubois , Jerome Lang , Henri Prade, Theorem proving under uncertainty: a possibility theory-based approach, Proceedings of the 10th international joint conference on Artificial intelligence, p.984-986, August 23-28, 1987, Milan, Italy
	Jieh Hsiang , Michael Rusinowitch , Ko Sakai, Complete inference rules for the cancellation laws, Proceedings of the 10th international joint conference on Artificial intelligence, p.990-992, August 23-28, 1987, Milan, Italy
	Robert F. Simmons , Daniel Chester, Inferences in quantified semantic networks, Proceedings of the 5th international joint conference on Artificial intelligence, p.267-273, August 22-25, 1977, Cambridge, USA
	C. L. Chang, Resolution plans in theorem proving, Proceedings of the 6th international joint conference on Artificial intelligence, p.143-148, August 20-23, 1979, Tokyo, Japan
	David Poole, First-order probabilistic inference, Proceedings of the 18th international joint conference on Artificial intelligence, p.985-991, August 09-15, 2003, Acapulco, Mexico
	Floriana Esposito , Nicola Fanizzi , Stefano Ferilli , Giovanni Semeraro, OI-implication: soundness and refutation completeness, Proceedings of the 17th international joint conference on Artificial intelligence, p.847-852, August 04-10, 2001, Seattle, WA, USA
	Robert Demolombe , Luis Farinas Del Cerro, An inference rule for hypothesis generation, Proceedings of the 12th international joint conference on Artificial intelligence, p.152-157, August 24-30, 1991, Sydney, New South Wales, Australia
	Katsumi Inoue, Consequence-finding based on ordered linear resolution, Proceedings of the 12th international joint conference on Artificial intelligence, p.158-164, August 24-30, 1991, Sydney, New South Wales, Australia
	Nicolas Helft , Katsumi Inoue , David Poole, Query answering in circumscription, Proceedings of the 12th international joint conference on Artificial intelligence, p.426-431, August 24-30, 1991, Sydney, New South Wales, Australia
	P. Adjiman , P. Chatalic , F. Goasdou´e , M.-C. Rousset , L. Simon, Scalability study of peer-to-peer consequence finding, Proceedings of the 19th international joint conference on Artificial intelligence, p.351-356, July 30-August 05, 2005, Edinburgh, Scotland
	Claudia d'Amato , Nicola Fanizzi , Floriana Esposito , Thomas Lukasiewicz, Approximate Classification of Semantically Annotated Web Resources Exploiting Pseudo-metrics Induced by Local Models, Proceedings of the 2009 IEEE/WIC/ACM International Joint Conference on Web Intelligence and Intelligent Agent Technology, p.689-692, September 15-18, 2009