ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
A Machine-Oriented Logic Based on the Resolution Principle
Full text PdfPdf (1.11 MB)
Source Journal of the ACM (JACM) archive
Volume 12 ,  Issue 1  (January 1965) table of contents
Pages: 23 - 41  
Year of Publication: 1965
ISSN:0004-5411
Author
J. A. Robinson  Argonne National Laboratory, Argonne, Illinois and Rice University, Houston, Texas
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 69,   Downloads (12 Months): 350,   Citation Count: 445
Additional Information:

references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/321250.321253
What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

 
1
CHURCH, A. A : noet the Eutchddugsproblem. J. symb Logic 1 (1936) 40-41. Correction ibid., 101-102.
2
Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960  [doi>10.1145/321033.321034]
3
Joyce Friedman, A Semi-Decision Procedure for the Functional Calculus, Journal of the ACM (JACM), v.10 n.1, p.1-24, Jan. 1963  [doi>10.1145/321150.321151]
 
4
GILMORE, P- C, A proof method for quantiFired ion theory. IBM J. Res. Develop. 4 (1960), 2S-35,
5
J. A. Robinson, Theorem-Proving on the Computer, Journal of the ACM (JACM), v.10 n.2, p.163-174, April 1963  [doi>10.1145/321160.321166]

CITED BY  448
James R. Slagle, Automatic Theorem Proving With Renamable and Semantic Resolution, Journal of the ACM (JACM), v.14 n.4, p.687-697, Oct. 1967
Rona B. Stillman, The Concept of Weak Substitution in Theorem-Proving, Journal of the ACM (JACM), v.20 n.4, p.648-667, Oct. 1973
Russell Greiner , Christian Darken , N. Iwan Santoso, Efficient reasoning, ACM Computing Surveys (CSUR), v.33 n.1, p.1-30, March 2001
Gordon V. Cormack , Andrew K. Wright, Type-dependent parameter inference, ACM SIGPLAN Notices, v.25 n.6, p.127-136, Jun. 1990
Barbara Smith , Ralph Wilkerson , Gerald E. Peterson, Automated circuit diagnosis using first order logic tools, Proceedings of the 1st international conference on Industrial and engineering applications of artificial intelligence and expert systems, p.456-465, June 1988, Tullahoma, Tennessee, United States
Gerald E. Peterson , Mark E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM (JACM), v.28 n.2, p.233-264, April 1981
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
Richard C. T. Lee, Fuzzy Logic and the Resolution Principle, Journal of the ACM (JACM), v.19 n.1, p.109-119, Jan. 1972
James R. Slagle, Automatic Theorem Proving with Built-in Theories Including Equality, Partial Ordering, and Sets, Journal of the ACM (JACM), v.19 n.1, p.120-135, Jan. 1972
P. C. Kanellakis , J. C. Mitchell, Polymorphic unification and ML typing, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-115, January 11-13, 1989, Austin, Texas, United States
Veronica Dahl, On database systems development through logic, ACM Transactions on Database Systems (TODS), v.7 n.1, p.102-123, March 1982
D. W. Loveland, A Simplified Format for the Model Elimination Theorem-Proving Procedure, Journal of the ACM (JACM), v.16 n.3, p.349-363, July 1969
Yatin Saraiya, Projection-propagation in complex-object query languages, Proceedings of the second international conference on Information and knowledge management, p.413-422, November 01-05, 1993, Washington, D.C., United States
Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico
Jean-Claude Raoult , Jean Vuillemin, Operational and semantic equivalence between recursive programs., Proceedings of the tenth annual ACM symposium on Theory of computing, p.75-85, May 01-03, 1978, San Diego, California, United States
Luca Cardelli , Peter Wegner, On understanding types, data abstraction, and polymorphism, ACM Computing Surveys (CSUR), v.17 n.4, p.471-523, Dec. 1985
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
David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.165-174, January 15-18, 1984, Salt Lake City, Utah, United States
L. J. Henschen, Theorem Proving by Covering Expressions, Journal of the ACM (JACM), v.26 n.3, p.385-400, july 1979
J. W. O'Toole, Jr. , D. K. Gifford, Type reconstruction with first-class polymorphic values, ACM SIGPLAN Notices, v.24 n.7, p.207-217, July 1989
J. Gu, Global Optimization for Satisfiability (SAT) Problem, IEEE Transactions on Knowledge and Data Engineering, v.6 n.3, p.361-381, June 1994
C. Cordell Green , Bertram Raphael, The use of theorem-proving techniques in question-answering systems, Proceedings of the 1968 23rd ACM national conference, p.169-181, August 27-29, 1968
Ping Gao , Robert Esser, Polymorphic CSP type checking, Australian Computer Science Communications, v.23 n.1, p.156-162, January-February 2001
Zhong Shao , Andrew W. Appel, Smartest recompilation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.439-450, March 1993, Charleston, South Carolina, 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
Kenneth A. Bowen, Prolog, Proceedings of the 1979 annual conference, p.14-23, January 1979
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
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
Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States
Henri E. Bal , Jennifer G. Steiner , Andrew S. Tanenbaum, Programming languages for distributed computing systems, ACM Computing Surveys (CSUR), v.21 n.3, p.261-322, Sep. 1989
Peter B. Andrews, Resolution With Merging, Journal of the ACM (JACM), v.15 n.3, p.367-381, July 1968
Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972
David N. Turner , Philip Wadler , Christian Mossin, Once upon a type, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.1-11, June 26-28, 1995, La Jolla, California, United States
M. Gordon , R. Milner , L. Morris , M. Newey , C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.119-130, January 23-25, 1978, Tucson, Arizona
Bertram Raphael, Aspects and applications of symbol manpulation, Proceedings of the 1966 21st national conference, p.69-74, January 1966
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
Ehud Shapiro, The family of concurrent logic programming languages, ACM Computing Surveys (CSUR), v.21 n.3, p.413-510, Sep. 1989
Christoph M. Hoffmann , Michael J. O'Donnell, Pattern Matching in Trees, Journal of the ACM (JACM), v.29 n.1, p.68-95, Jan. 1982
Ehud Y. Shapiro, The fifth generation project — a trip report, Communications of the ACM, v.26 n.9, p.637-641, Sept. 1983
F. N. Sibai , L. Watson , M. Lu, Design and performance measurements of a parallel machine for the unification algorithm, ACM SIGMICRO Newsletter, v.20 n.3, p.21-30, Sep. 1989
Tomasz Pietrzykowski, A Complete Mechanization of Second-Order Type Theory, Journal of the ACM (JACM), v.20 n.2, p.333-364, April 1973
Burt M. Leavenoworth , Jean E. Sammet, An overview of nonprocedural languages, ACM SIGPLAN Notices, v.9 n.4, p.1-12, April 1974
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
Amaryllis Deliyanni , Robert A. Kowalski, Logic and semantic networks, Communications of the ACM, v.22 n.3, p.184-192, March 1979
Daniel Murphy, Unification for completely commutative theories, Proceedings of the 1992 ACM/SIGAPP Symposium on Applied computing: technological challenges of the 1990's, p.547-553, April 1992, Kansas City, Missouri, United States
John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States
Alain Colmerauer, Prolog in 10 figures, Communications of the ACM, v.28 n.12, p.1296-1310, Dec. 1985
J. R. Quinlan , E. B. Hunt, A Formal Deductive Problem-Solving System, Journal of the ACM (JACM), v.15 n.4, p.625-646, Oct. 1968
T. Pietrzykowski , D. C. Jensen, A complete mechanization of (&ohgr;) -order type theory, Proceedings of the ACM annual conference, p.82-92, August 01-01, 1972, Boston, Massachusetts, United States
Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980
Chang-Shing Perng , Haixun Wang , Sheng Ma , Joseph L. Hellerstein, Discovery in multi-attribute data with user-defined constraints, ACM SIGKDD Explorations Newsletter, v.4 n.1, June 2002
Uday S. Reddy, Transformational derivation of programs using the focus system, ACM SIGSOFT Software Engineering Notes, v.13 n.5, p.163-172, November 1988
Carsten K. Gomard, Partial type inference for untyped functional programs, Proceedings of the 1990 ACM conference on LISP and functional programming, p.282-287, June 27-29, 1990, Nice, France
Mark P. Jones, A system of constructor classes: overloading and implicit higher-order polymorphism, Proceedings of the conference on Functional programming languages and computer architecture, p.52-61, June 09-11, 1993, Copenhagen, Denmark
Grigoris Antoniou , David Billington , Guido Governatori , Michael J. Maher, Representation results for defeasible logic, ACM Transactions on Computational Logic (TOCL), v.2 n.2, p.255-287, April 2001
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
C. J. Hogger, Derivation of Logic Programs, Journal of the ACM (JACM), v.28 n.2, p.372-392, April 1981
Scott Danforth , Chris Tomlinson, Type theories and object-oriented programmimg, ACM Computing Surveys (CSUR), v.20 n.1, p.29-72, March 1988
G. Gottlob, Computing covers for embedded functional dependencies, Proceedings of the sixth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.58-69, March 23-25, 1987, San Diego, California, United States
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
Ralph W. Wilkerson , Blayne E. Mayfield, The role of term symmetry in E-completion procedures, Proceedings of the 1990 ACM annual conference on Cooperation, p.134-139, February 20-22, 1990, Washington, D.C., United States
Raymond Reiter, The predicate elimination strategy in theorem proving, Proceedings of the second annual ACM symposium on Theory of computing, p.180-183, May 04-06, 1970, Northampton, Massachusetts, United States
Robert M. Schwarcz , John F. Burger , Robert F. Simmons, A deductive question-answerer for natural language inference, Communications of the ACM, v.13 n.3, p.167-183, March 1970
Alexander Aiken , Edward L. Wimmers, Type inclusion constraints and type inference, Proceedings of the conference on Functional programming languages and computer architecture, p.31-41, June 09-11, 1993, Copenhagen, Denmark
Mark E. Stickel, A Unification Algorithm for Associative-Commutative Functions, Journal of the ACM (JACM), v.28 n.3, p.423-434, July 1981
Aleksy Schubert, Second-order unification and type inference for Church-style polymorphism, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.279-288, January 19-21, 1998, San Diego, California, United States
M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976
Wolfgang Bibel, On Matrices with Connections, Journal of the ACM (JACM), v.28 n.4, p.633-645, Oct. 1981
Olivier Coudert , Tsutomu Sasao, Two-level logic minimization, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
C. H. Kung, On verification of database temporal constraints, ACM SIGMOD Record, v.14 n.4, p.169-179, May 1985
Brian Reistad , David K. Gifford, Static dependent costs for estimating execution time, ACM SIGPLAN Lisp Pointers, v.VII n.3, p.65-78, July-Sept. 1994
M. Baudinet, Temporal logic programming is complete and expressive, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.267-280, January 11-13, 1989, Austin, Texas, United States
Seif Haridi , Peter Van Roy , Per Brand , Michael Mehl , Ralf Scheidhauer , Gert Smolka, Efficient logic variables for distributed computing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.569-626, May 1999
Oukseh Lee , Kwangkeun Yi, Proofs about a folklore let-polymorphic type inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.707-723, July 1998
Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982
Alain Colmerauer , Philippe Roussel, The birth of Prolog, ACM SIGPLAN Notices, v.28 n.3, p.37-52, March 1993
John Grant , Jack Minker, The impact of logic programming on databases, Communications of the ACM, v.35 n.3, p.66-81, March 1992
Lawrence Wos , George A. Robinson , Daniel F. Carson , Leon Shalla, The Concept of Demodulation in Theorem Proving, Journal of the ACM (JACM), v.14 n.4, p.698-709, Oct. 1967
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
Johan de Kleer , Jon Doyle , Guy L. Steele, Jr. , Gerald Jay Sussman, AMORD explicit control of reasoning, ACM SIGPLAN Notices, v.12 n.8, p.116-125, August 1977
Richard Rankin, Increasing the efficiency of Prolog Lexical databases with N-gram Boolean cubes, Proceedings of the 1988 ACM SIGSMALL/PC symposium on ACTES, p.161-166, May 04-06, 1988, Cannes, France
H. Gaifman , E. Shapiro, Fully abstract compositional semantics for logic programs, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.134-142, January 11-13, 1989, Austin, Texas, United States
K. A. Yelick , J. L. Zachary, Moded type systems for logic programming, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.116-124, January 11-13, 1989, Austin, Texas, United States
Peter Buneman , Atsushi Ohori, Polymorphism and type inference in database programming, ACM Transactions on Database Systems (TODS), v.21 n.1, p.30-76, March 1996
William H. Joiner, Jr., Resolution Strategies as Decision Procedures, Journal of the ACM (JACM), v.23 n.3, p.398-417, July 1976
Alain Colmerauer, An introduction to Prolog III, Communications of the ACM, v.33 n.7, p.69-90, July 1990
Mitchell Wand, A types-as-sets semantics for milner-style polymorphism, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.158-164, January 15-18, 1984, Salt Lake City, Utah, United States
Fritz Henglein , Harry G. Mairson, The complexity of type inference for higher-order lambda calculi, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-130, January 21-23, 1991, Orlando, Florida, United States
Jean-Claude Raoult , Jean Vuillemin, Operational and Semantic Equivalence Between Recursive Programs, Journal of the ACM (JACM), v.27 n.4, p.772-796, Oct. 1980
Daniel R. Dolk, A generalized model management system for mathematical programming, ACM Transactions on Mathematical Software (TOMS), v.12 n.2, p.92-126, June 1986
R. Ghosh-Roy , Frank Jensen, Conjunctional type assignment in programming languages, Proceedings of the 1988 ACM sixteenth annual conference on Computer science, p.475-482, February 1988, Atlanta, Georgia, United States
Alon Kleinman , Yoram Moses , Ehud Shapiro, Distributed variable server for atomic unification, Proceedings of the ninth annual ACM symposium on Principles of distributed computing, p.59-74, August 22-24, 1990, Quebec City, Quebec, Canada
Robert Kowalski, A Proof Procedure Using Connection Graphs, Journal of the ACM (JACM), v.22 n.4, p.572-595, Oct. 1975
Jack Minker, Search strategy and selection function for an inferential relational system, ACM Transactions on Database Systems (TODS), v.3 n.1, p.1-31, March 1978
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
D. W. Loveland, A Unifying View of Some Linear Herbrand Procedures, Journal of the ACM (JACM), v.19 n.2, p.366-384, April 1972
Donald W. Loveland, Mechanical Theorem-Proving by Model Elimination, Journal of the ACM (JACM), v.15 n.2, p.236-251, April 1968
Norman Rubin , Malcolm C. Harrison, Another Generalization of Resolution, Journal of the ACM (JACM), v.25 n.3, p.341-351, July 1978
T. Watanabe , T. Masuishi , T. Nishiyama , N. Horie, Knowledge-based optimal IIL generator from conventional logic circuit descriptions, Proceedings of the 23rd ACM/IEEE conference on Design automation, p.608-614, July 1986, Las Vegas, Nevada, United States
Chris Merz , W. E. Bond , Dan St. Clair, Matching interval-valued-argument propositions in rule-based systems, Proceedings of the 1990 ACM annual conference on Cooperation, p.343-350, February 20-22, 1990, Washington, D.C., United States
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
Robert Anderson , W. W. Bledsoe, A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness, Journal of the ACM (JACM), v.17 n.3, p.525-534, July 1970
Mitchell Wand, A semantic prototyping system, ACM SIGPLAN Notices, v.19 n.6, p.213-221, June 1984
Rolf Bahlke , Gregor Snelting, The PSG system: from formal language definitions to interactive programming environments, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.4, p.547-576, Oct. 1986
Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993
Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965
Gene Cooperman, STAR/MPI: binding a parallel library to interactive symbolic algebra systems, Proceedings of the 1995 international symposium on Symbolic and algebraic computation, p.126-132, July 10-12, 1995, Montreal, Quebec, Canada
Craig Stanfill , David Waltz, Toward memory-based reasoning, Communications of the ACM, v.29 n.12, p.1213-1228, Dec. 1986
Vašek Chvátal , Endre Szemerédi, Many hard examples for resolution, Journal of the ACM (JACM), v.35 n.4, p.759-768, Oct. 1988
Arthur J. Nevins, A Human Oriented Logic for Automatic Theorem-Proving, Journal of the ACM (JACM), v.21 n.4, p.606-621, Oct. 1974
Michael Fisher , Clare Dixon , Martin Peim, Clausal temporal resolution, ACM Transactions on Computational Logic (TOCL), v.2 n.1, p.12-56, Jan. 2001
César Muñoz, Proof-term synthesis on dependent-type systems via explicit substitutions, Theoretical Computer Science, v.266 n.1-2, p.407-440, 09/06/2001
John K. Dixon, Z-Resolution: Theorem-Proving with Compiled Axioms, Journal of the ACM (JACM), v.20 n.1, p.127-147, Jan. 1973
Edward E. Balkovich , George P. Engelberg, Research towards a technology to support the specification of data processing system performance requirements, Proceedings of the 2nd international conference on Software engineering, p.110-115, October 13-15, 1976, San Francisco, California, United States
Ramin Yasdi, Formal representation of a conceptual knowledge model for a database based expert system, Proceedings of the twenty-first annual conference on Computer personnel research, p.11-23, May 02-03, 1985, Minneapolis, Minnesota, United States
Stephen Cook , Robert Reckhow, On the lengths of proofs in the propositional calculus (Preliminary Version), Proceedings of the sixth annual ACM symposium on Theory of computing, p.135-148, April 30-May 02, 1974, Seattle, Washington, 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
P. A. Subrahmanyam , J-H. You, Pattern driven lazy reduction: A unifying evaluation mechanism for functional and logic programs, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.228-234, January 15-18, 1984, Salt Lake City, Utah, United States
Jacques Cohen, A view of the origins and development of Prolog, Communications of the ACM, v.31 n.1, p.26-36, Jan. 1988
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
Robert A. Kowalski, The early years of logic programming, Communications of the ACM, v.31 n.1, p.38-43, Jan. 1988
Gordon Beavers , Hal Berghel, “Dynamic” inferencing with generalized resolution, Proceedings of the 1993 ACM/SIGAPP symposium on Applied computing: states of the art and practice, p.614-621, February 14-16, 1993, Indianapolis, Indiana, United States
Martín Abadi , Zohar Manna, Nonclausal deduction in first-order temporal logic, Journal of the ACM (JACM), v.37 n.2, p.279-317, April 1990
Zohar Manna, Properties of Programs and the First-Order Predicate Calculus, Journal of the ACM (JACM), v.16 n.2, p.244-255, April 1969
An introduction to inductive logic programming, Relational Data Mining, Springer-Verlag New York, Inc., New York, NY, 2001
George W. Ernst, Sufficient Conditions for the Success of GPS, Journal of the ACM (JACM), v.16 n.4, p.517-533, Oct. 1969
Kung Chen , Paul Hudak , Martin Odersky, Parametric type classes, ACM SIGPLAN Lisp Pointers, v.V n.1, p.170-181, Jan. 1992
Luca Cardelli, Compiling a functional language, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.208-217, August 06-08, 1984, Austin, Texas, United States
Mitch Cherniack , Stanley B. Zdonik, Rule languages and internal algebras for rule-based optimizers, ACM SIGMOD Record, v.25 n.2, p.401-412, June 1996
Evgeny Dantsin , Thomas Eiter , Georg Gottlob , Andrei Voronkov, Complexity and expressive power of logic programming, ACM Computing Surveys (CSUR), v.33 n.3, p.374-425, September 2001
Bharat Jayaraman , Frank S. K. Silbermann, Equations, sets, and reduction semantics for functional and logic programming, Proceedings of the 1986 ACM conference on LISP and functional programming, p.320-331, August 1986, Cambridge, Massachusetts, United States
Ross A. Overbeek, A New Class of Automated Theorem-Proving Algorithms, Journal of the ACM (JACM), v.21 n.2, p.191-200, April 1974
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
Zvi Galil, On the validity and complexity of bounded resolution, Proceedings of seventh annual ACM symposium on Theory of computing, p.72-82, May 05-07, 1975, Albuquerque, New Mexico, United States
Jack Minker, Introduction to logic-based artificial intelligence, Logic-based artificial intelligence, Kluwer Academic Publishers, Norwell, MA, 2000
María García de la Banda , Manuel Hermenegildo , Kim Marriott, Independence in CLP languages, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.296-339, March 2000
Yonathan Malachi , Zohar Manna , Richard Waldinger, TABLOG: The deductive-tableau programming language, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.323-330, August 06-08, 1984, Austin, Texas, United States
Atsushi Ohori , Peter Buneman, Type inference in a database programming language, Proceedings of the 1988 ACM conference on LISP and functional programming, p.174-183, July 25-27, 1988, Snowbird, Utah, United States
Nicolas Peltier, Extracting models from clause sets saturated under semantic refinements of the resolution rule, Information and Computation, v.181 n.2, p.99-130, March 15, 2003
Christoph Walther, Many-sorted unification, Journal of the ACM (JACM), v.35 n.1, p.1-17, Jan. 1988
James A. Brown , Janice H. Cook , Leo H. Groner , Ed Eusebi, Logic programming in APL2, ACM SIGAPL APL Quote Quad, v.16 n.4, p.282-288, 1986
Gregory F. Johnson , Janet A. Walz, A maximum-flow approach to anomaly isolation in unification-based incremental type inference, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.44-57, January 01, 1986, St. Petersburg Beach, Florida
Alexander Razborov , Avi Wigderson , Andrew Yao, Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus, Proceedings of the twenty-ninth annual ACM symposium on Theory of computing, p.739-748, May 04-06, 1997, El Paso, Texas, United States
G. Gottlob , A. Leitsch, On the efficiency of subsumption algorithms, Journal of the ACM (JACM), v.32 n.2, p.280-295, April 1985
P. A. Subrahmanyam, LCS—a leaf cell synthesizer employing formal deduction techniques, Proceedings of the 24th ACM/IEEE conference on Design automation, p.459-465, June 28-July 01, 1987, Miami Beach, Florida, United States
Marc Denecker , Maurice Bruynooghe , Victor Marek, Logic programming revisited: logic programs as inductive definitions, ACM Transactions on Computational Logic (TOCL), v.2 n.4, p.623-654, Oct. 2001
Mark P. Jones, First-class polymorphism with type inference, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.483-496, January 15-17, 1997, Paris, France
Lawrence J. Henschen , Shamim A. Naqvi, On compiling queries in recursive first-order databases, Journal of the ACM (JACM), v.31 n.1, p.47-85, Jan. 1984
Atsushi Ohori, A polymorphic record calculus and its compilation, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.6, p.844-895, Nov. 1995
Drew McDermott, Nonmonotonic Logic II: Nonmonotonic Modal Theories, Journal of the ACM (JACM), v.29 n.1, p.33-57, Jan. 1982
Mads Tofte, Principal signatures for higher-order program modules, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.189-199, January 19-22, 1992, Albuquerque, New Mexico, United States
Chris Clifton , Hector Garcie-Molina, The design of a document database, Proceedings of the ACM conference on Document processing systems, p.125-134, December 05-08, 1988, Santa Fe, New Mexico, United States
Norihisa Suzuki, Inferring types in Smalltalk, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.187-199, January 26-28, 1981, Williamsburg, Virginia
Jacques Cohen, Logic programming and constraint logic programming, ACM Computing Surveys (CSUR), v.28 n.1, p.257-259, March 1996
J. I. Glasgow , M. A. Jenkins , E. Blevis , M. P. Féret, Logic Programming with Arrays, IEEE Transactions on Knowledge and Data Engineering, v.3 n.3, p.307-319, September 1991
C. L. Chang, The Unit Proof and the Input Proof in Theorem Proving, Journal of the ACM (JACM), v.17 n.4, p.698-707, Oct. 1970
Keith L. Clark , Steve Gregory, A relational language for parallel programming, Proceedings of the 1981 conference on Functional programming languages and computer architecture, p.171-178, October 18-22, 1981, Portsmouth, New Hampshire, United States
Richard B. Kieburtz, Precise typing of abstract data type specifications, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.109-116, January 24-26, 1983, Austin, Texas
David H D Warren , Luis M. Pereira , Fernando Pereira, Prolog - the language and its implementation compared with Lisp, ACM SIGPLAN Notices, v.12 n.8, p.109-115, August 1977
Takuya Katayama, Type inference and type checking for functional programming languages: A reduced computation approach, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.263-272, August 06-08, 1984, Austin, Texas, United States
Kevin Knight, Unification: a multidisciplinary survey, ACM Computing Surveys (CSUR), v.21 n.1, p.93-124, March 1989
Alasdair Urquhart, Hard examples for resolution, Journal of the ACM (JACM), v.34 n.1, p.209-219, Jan. 1987
Alexander A. Razborov, Resolution lower bounds for the weak functional pigeonhole principle, Theoretical Computer Science, v.303 n.1, p.233-243, 28 June 2003
Johannes Grabmeier , Erich Kaltofen , Volker Weispfenning, Cited References, Computer algebra handbook, Springer-Verlag New York, Inc., New York, NY, 2003
Gregor Snelting , Wolfgang Henhapl, Unification in many-sorted algebras as a device for incremental semantic analysis, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.229-235, January 01, 1986, St. Petersburg Beach, Florida
Matthias Baaz , Christian G. Fermüller , Gernot Salzer, Automated deduction for many-valued logics, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
Christian G. Fermüller , Alexander Leitsch , Ullrich Hustadt , Tanel Tammet, Resolution decision procedures, 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
Sergei Abramov , Robert Glück, Principles of inverse computation and the Universal resolving algorithm, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
Reinhard Pichler, On the complexity of equational problems in CNF, Journal of Symbolic Computation, v.36 n.1-2, p.235-269, July 2003
H. Jan Komorowski, Partial evaluation as a means for inferencing data structures in an applicative language: a theory and implementation in the case of prolog, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.255-267, January 25-27, 1982, Albuquerque, Mexico
Remko Scha , Livia Polanyi, An augmented context free grammar for discourse, Proceedings of the 12th conference on Computational linguistics, p.573-577, August 22-27, 1988, Budapest, Hungry
Marco Bellia , M. Eugenia Occhiuto, N-axioms parallel unification, Fundamenta Informaticae, v.55 n.2, p.115-128, May 2003
Hendrik Blockeel , Michèle Sebag, Scalability and efficiency in multi-relational data mining, ACM SIGKDD Explorations Newsletter, v.5 n.1, July 2003
Juan Luis Esteban , Jacobo Torán, A combinatorial characterization of treelike resolution space, Information Processing Letters, v.87 n.6, p.295-300, 30 September 2003
Wei Li , Shilong Ma, Limits of theory sequences over algebraically closed fields and applications, Discrete Applied Mathematics, v.136 n.1, p.23-43, 30 January 2004
Fernando Pereira, Review of "The logic of typed feature structures" by Bob Carpenter. Cambridge University Press 1992., Computational Linguistics, v.19 n.3, September 1993
Fernando C. N. Pereira , David H. D. Warren, Parsing as deduction, Proceedings of the 21st annual meeting on Association for Computational Linguistics, June 15-17, 1983, Cambridge, Massachusetts
Marcia A. Derr , Kathleen R. McKeown, Using focus to generate complex and simple sentences, Proceedings of the 22nd annual meeting on Association for Computational Linguistics, p.319-326, July 02-06, 1984, Stanford, California
Albert Atserias, On sufficient conditions for unsatisfiability of random formulas, Journal of the ACM (JACM), v.51 n.2, p.281-311, March 2004
Robert J. P. Ingria, The limits of unification, Proceedings of the 28th annual meeting on Association for Computational Linguistics, p.194-204, June 06-09, 1990, Pittsburgh, Pennsylvania
J. A. Robinson, Logic and logic programming, Communications of the ACM, v.35 n.3, p.40-65, March 1992
Zohar Manna , Richard Waldinger, Special relations in automated deduction, Journal of the ACM (JACM), v.33 n.1, p.1-59, Jan. 1986
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
Lalita Jategaonkar , John Mitchell, ML with extended pattern matching and subtypes, Proceedings of the 1988 ACM conference on LISP and functional programming, p.198-211, July 25-27, 1988, Snowbird, Utah, United States
S. Fleisig , D. Loveland , A. K. Smiley, III , D. L. Yarmush, An Implementation of the Model Elimination Proof Procedure, Journal of the ACM (JACM), v.21 n.1, p.124-139, Jan. 1974
C. L. Chang , J. R. Slagle, Completeness of Linear Refutation for Theories with Equality, Journal of the ACM (JACM), v.18 n.1, p.126-136, Jan. 1971
R. C. T. Lee , R. J. Waldinger , C. L. Chang, An improved program-synthesizing algorithm and its correctness, Communications of the ACM, v.17 n.4, p.211-217, April 1974
P. Raulefs , J. Siekmann , P. Szabó , E. Unvericht, A short survey on the state of the art in matching and unification problems, ACM SIGSAM Bulletin, v.13 n.2, p.14-20, May 1979
Stavros Tripakis , Christos Sofronis , Paul Caspi , Adrian Curic, Translating discrete-time simulink to lustre, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.4, p.779-818, November 2005
Daniel Leivant, Polymorphic type inference, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.88-98, January 24-26, 1983, Austin, Texas
Raymond Reiter, Two Results on Ordering for Resolution with Merging and Linear Format, Journal of the ACM (JACM), v.18 n.4, p.630-646, Oct. 1971
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
Richard J. Waldinger , Karl N. Levitt, Reasoning about programs, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.169-182, October 01-03, 1973, Boston, Massachusetts
Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980
Zohar Manna , Richard J. Waldinger, Toward automatic program synthesis, Communications of the ACM, v.14 n.3, p.151-165, March 1971
John Franco, Results related to threshold phenomena research in satisfiability: lower bounds, Theoretical Computer Science, v.265 n.1_2, p.147-157, 08/28/2001
James R. Slagle, Interpolation Theorems for Resolution in Lower Predicate Calculus, Journal of the ACM (JACM), v.17 n.3, p.535-542, July 1970
F. N. Sibai , K. L. Watson , Mi Lu, A Parallel Unification Machine, IEEE Micro, v.10 n.4, p.21-33, July 1990
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
Fujio Nishida , Shinobu Takamatsu , Yoneharu Fujita , Tadaaki Tani, Semi-Automatic Program Construction from Specifications Using Library Modules, IEEE Transactions on Software Engineering, v.17 n.9, p.853-871, September 1991
Chee-Fen Yu , Benjamin W. Wah, Learning Dominance Relations in Combined Search Problems, IEEE Transactions on Software Engineering, v.14 n.8, p.1155-1175, August 1988
J. Naganuma , T. Ogura , S.-I. Yamada , T. Kimura, High-Speed CAM-Based Architecture for a Prolog Machine (ASCA), IEEE Transactions on Computers, v.37 n.11, p.1375-1383, November 1988
Saumya K. Debray , David S. Warren, Towards Banishing the Cut from Prolog, IEEE Transactions on Software Engineering, v.16 n.3, p.335-349, March 1990
Stuart J. Russell, An architecture for bounded rationality, ACM SIGART Bulletin, v.2 n.4, p.146-150, Aug. 1991
Raymond Reiter, Formal reasoning and language understanding systems, Proceedings of the 1975 workshop on Theoretical issues in natural language processing, June 10-13, 1975, Cambridge, Massachusetts
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
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
Nicolas Peltier, Constructing decision procedures in equational clausal logic, Fundamenta Informaticae, v.54 n.1, p.17-65, January 2003
Sabine Glesner , Wolf Zimmermann, Natural semantics as a static program analysis framework, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.3, p.510-577, May 2004
Jérôme Maloberti , Michèle Sebag, Fast Theta-Subsumption with Constraint Satisfaction Algorithms, Machine Learning, v.55 n.2, p.137-174, May 2004
Clemens Ballarin , Manuel Kauers, Solving parametric linear systems: an experiment with constraint algebraic programming, ACM SIGSAM Bulletin, v.38 n.2, June 2004
Silvano Di Zenzo, A many-valued logic for approximate reasoning, IBM Journal of Research and Development, v.32 n.4, p.552-565, July 1988
Carlos Camarão , Lucília Figueiredo , Cristiano Vasconcellos, Constraint-set satisfiability for overloading, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.67-77, August 24-26, 2004, Verona, Italy
Christophe Geissler , Kurt Konolige, A resolution method for quantified modal logics of knowledge and belief, Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, March 19-22, 1986, Monterey, California
David C. Luckham , James Vera, An Event-Based Architecture Definition Language, IEEE Transactions on Software Engineering, v.21 n.9, p.717-734, September 1995
Drew McDermott, Artificial intelligence meets natural stupidity, ACM SIGART Bulletin
C. Barry Jay, The pattern calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.6, p.911-937, November 2004
Matthew Stone, Disjunction and modular goal-directed proof search, ACM Transactions on Computational Logic (TOCL), v.6 n.3, p.539-577, July 2005
Ernest Teniente , Toni Urpí, Checking query containment with the CQC method, Data & Knowledge Engineering, v.53 n.2, p.163-223, May 2005
Ştefan Andrei, Counting for Satisfiability by Inverting Resolution, Artificial Intelligence Review, v.22 n.4, p.339-366, December 2004
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
A. Browne , J. Pilkington, Unification using a distributed representation, ACM SIGART Bulletin, v.5 n.2, p.5-7, April 1994
Eli Ben-Sasson, Size space tradeoffs for resolution, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
Lambert Meertens, Incremental polymorphic type checking in B, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.265-275, January 24-26, 1983, Austin, Texas
C. S. Mellish, Implementing systemic classification by unification, Computational Linguistics, v.14 n.1, p.40-51, Winter 1988
James Kilbury, A proposal for modifications in the formalism of GPSG, Proceedings of the third conference on European chapter of the Association for Computational Linguistics, p.156-159, April 01-03, 1987, Copenhagen, Denmark
Jun Gu , Qian-Ping Gu , Ding-Zhu Du, Convergence Properties of Optimization Algorithms for the SAT Problem, IEEE Transactions on Computers, v.45 n.2, p.209-218, February 1996
Donald MacKenzie, The Automation of Proof: A Historical and Sociological Exploration, IEEE Annals of the History of Computing, v.17 n.3, p.7-29, September 1995
Jack Minker, Control structure of a pattern-directed search system, ACM SIGART Bulletin
Donald MacKenzie, The Automation of Proof: A Historical and Sociological Exploration, IEEE Annals of the History of Computing, v.17 n.3, p.7-29, September 1995
Andreas Meier , Martin Pollet , Volker Sorge, Comparing approaches to the exploration of the domain of residue classes, Journal of Symbolic Computation, v.34 n.4, p.287-306, October 2002
Lubomir Bic, The Fifth Generation grail: A survey of related research, Proceedings of the 1984 annual conference of the ACM on The fifth generation challenge, p.293-297, January 1984
Jörg-Uwe Kietz , Sašo Džeroski, Inductive logic programming and learnability, ACM SIGART Bulletin, v.5 n.1, p.22-32, Jan. 1994
Deborah East , Miroslaw Truszczyński, Predicate-calculus-based logics for modeling and solving search problems, ACM Transactions on Computational Logic (TOCL), v.7 n.1, p.38-83, January 2006
Marco Cadoli , Marco Schaerf, Approximate reasoning and non-omniscient agents, Proceedings of the 4th conference on Theoretical aspects of reasoning about knowledge, p.169-183, March 22-25, 1992, Monterey, California
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
Zohar Manna , Richard Waldinger, Fundamentals of Deductive Program Synthesis, IEEE Transactions on Software Engineering, v.18 n.8, p.674-704, August 1992
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
Alain Colmerauer , Philippe Roussel, The birth of Prolog, History of programming languages---II, ACM Press, New York, NY, 1996
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
Ken Q. Pu, Modeling, querying and reasoning about OLAP databases: a functional approach, Proceedings of the 8th ACM international workshop on Data warehousing and OLAP, November 04-05, 2005, Bremen, Germany
Jack Minker, Information storage and retrieval: a survey and functional description, ACM SIGIR Forum, v.12 n.2, p.12-108, Fall 1977
Paolo Liberatore, Complexity results on DPLL and resolution, ACM Transactions on Computational Logic (TOCL), v.7 n.1, p.84-107, January 2006
Venkatesh Choppella , Christopher T. Haynes, Source-tracking unification, Information and Computation, v.201 n.2, p.121-159, September 15, 2005
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
Arild Waaler, Connections in nonclassical logics, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
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
Veronica Dahl , Michael C. McCord, Treating coordination in logic grammars, Computational Linguistics, v.9 n.2, p.69-80, April-June 1983
John Franco, Typical case complexity of satisfiability algorithms and the threshold phenomenon, Discrete Applied Mathematics, v.153 n.1, p.89-123, 1 December 2005
Matthew Richardson , Pedro Domingos, Markov logic networks, Machine Learning, v.62 n.1-2, p.107-136, February 2006
C. A. Johnson, Factorization and circuit in the connection method, Journal of the ACM (JACM), v.40 n.3, p.536-557, July 1993
Jakob Nordström, Narrow proofs may be spacious: separating space and width in resolution, Proceedings of the thirty-eighth annual ACM symposium on Theory of computing, May 21-23, 2006, Seattle, WA, USA
Hassan Aït-Kaci , Roger Nasr, Logic and inheritance, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.219-228, January 01, 1986, St. Petersburg Beach, Florida
Christian Jacquemin, A temporal connectionist approach to natural language, ACM SIGART Bulletin, v.5 n.3, p.12-22, July 1994
Andrew Haas, A parsing algorithm for unification grammar, Computational Linguistics, v.15 n.4, p.219-232, December 1989
J. Herath , Y. Yamaguchi , N. Saito , T. Yuba, Dataflow Computing Models, Languages, and Machines for Intelligence Computations, IEEE Transactions on Software Engineering, v.14 n.12, p.1805-1828, December 1988
Dominic Duggan , John Ophel, Open and closed scopes for constrained genericity, Theoretical Computer Science, v.275 n.1-2, p.215-258, March 28 2002
Khalil Djelloul, Decomposable theories, Theory and Practice of Logic Programming, v.7 n.5, p.583-632, September 2007
Jan Friso Groote , Joost P. Warners, The Propositional Formula Checker HeerHugo, Journal of Automated Reasoning, v.24 n.1-2, p.101-125, February 2000
Carsten Sinz, Visualizing SAT Instances and Runs of the DPLL Algorithm, Journal of Automated Reasoning, v.39 n.2, p.219-243, August 2007
Floriana Esposito , Nicola Fanizzi , Stefano Ferilli , Giovanni Semeraro, A Generalization Model Based on OI-implication for Ideal heory Refinement, Fundamenta Informaticae, v.47 n.1-2, p.15-33, January 2001
Mohand-Saïd Hacid , Farouk Toumani , Ahmed K. Elmagarmid, Constraint-Based Approach to Semistructured Data, Fundamenta Informaticae, v.47 n.1-2, p.53-73, January 2001
Peter B. Andrews, Herbrand Award Acceptance Speech, Journal of Automated Reasoning, v.31 n.2, p.169-187, 2003
A. V. Lyaletski, Evidential Paradigm: The Logical Aspect, Cybernetics and Systems Analysis, v.39 n.5, p.659-667, September-October 2003
Zbigniew Stachniak, Non-Clausal Reasoning with Definite Theories, Fundamenta Informaticae, v.48 n.4, p.363-388, December 2001
Khalil Djelloul , Thi-Bich-Hanh Dao, Solving first-order constraints in the theory of finite or infinite trees: introduction to the decomposable theories, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
Vincent J. Digricoli , Malcolm C. Harrison, Equality-based binary resolution, Journal of the ACM (JACM), v.33 n.2, p.253-289, April 1986
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
Ken Kaneiwa, A hybrid reasoning system for terminologies and first-order clauses in knowledge bases, New Generation Computing, v.24 n.1, p.29-51, January 2006
Sandra Alves , Mário Florido, Weak linearization of the lambda calculus, Theoretical Computer Science, v.342 n.1, p.79-103, 6 September 2005
Yacine Sam , Omar Boucelma , Mohand-Saïd Hacid, web services customization: a composition-based approach, Proceedings of the 6th international conference on Web engineering, July 11-14, 2006, Palo Alto, California, USA
Michelangelo Ceci , Annalisa Appice, Spatial associative classification: propositional vs structural approach, Journal of Intelligent Information Systems, v.27 n.3, p.191-213, November 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
Lucas Bordeaux , Youssef Hamadi , Lintao Zhang, Propositional Satisfiability and Constraint Programming: A comparative survey, ACM Computing Surveys (CSUR), v.38 n.4, p.12-es, 2006
Temur Kutsia, Solving equations with sequence variables and sequence functions, Journal of Symbolic Computation, v.42 n.3, p.352-388, March, 2007
David Poole , Alan Mackworth, Dimensions of complexity of intelligent agents, Proceedings of the 2006 international symposium on Practical cognitive agents and robots, November 27-28, 2006, Perth, Australia
Kenryo Indo, Proving Arrow's theorem by PROLOG, Computational Economics, v.30 n.1, p.57-63, August 2007
Pramod G. Joisha , Prithviraj Banerjee, An algebraic array shape inference system for MATLAB®, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.5, p.848-907, September 2006
Eric Kow, GenI: natural language generation in Haskell, Proceedings of the 2006 ACM SIGPLAN workshop on Haskell, September 17-17, 2006, Portland, Oregon, USA
Charles Kellogg , Philip Klahr , Larry Travis, A deductive capability for data management, Proceedings of the second international conference on Systems for Large Data Bases, p.181-196, September 08-10, 1976, Brussels, Belgium, North Holland
Yannis E. Ioannidis, A time bound on the materialization of some recursively defined views, Proceedings of the 11th international conference on Very Large Data Bases, p.219-226, August 21-23, 1985, Stockholm, Sweden
David H. D. Warren, Efficient processing of interactive relational data base queries expressed in logic, Proceedings of the seventh international conference on Very Large Data Bases, p.272-281, September 09-11, 1981, Cannes, France
Verónica Dahl, Logical design of deductive natural language consultable data bases, Proceedings of the fifth international conference on Very Large Data Bases, p.24-31, October 03-05, 1979, Rio de Janeiro, Brazil
Bahareh Badban , Jaco van de Pol , Olga Tveretina , Hans Zantema, Generalizing DPLL and satisfiability for equalities, Information and Computation, v.205 n.8, p.1188-1211, August, 2007
Brad Lushman , Gordon V. Cormack, A larger decidable semiunification problem, Proceedings of the 9th ACM SIGPLAN international symposium on Principles and practice of declarative programming, July 14-16, 2007, Wroclaw, Poland
Khalil Djelloul , Thi-Bich-Hanh Dao , Thom Fruehwirth, Toward a first-order extension of Prolog's unification using CHR: a CHR first-order constraint solver over finite or infinite trees, Proceedings of the 2007 ACM symposium on Applied computing, March 11-15, 2007, Seoul, Korea
Nicolas Peltier, Extended resolution simulates binary decision diagrams, Discrete Applied Mathematics, v.156 n.6, p.825-837, March, 2008
Bernard Lang, Matching with multiplication and exponentiation (extended abstract), Mathematical Structures in Computer Science, v.15 n.5, p.959-968, October 2005
A. Glebov , S. Gavrilov , R. Soloviev , V. Zolotov , M. R. Becer , C. Oh , R. Panda, Delay noise pessimism reduction by logic correlations, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.160-167, November 07-11, 2004
Alexander Serebrenik , Danny Schreye, Termination of Floating-Point Computations, Journal of Automated Reasoning, v.34 n.2, p.141-177, December 2005
A. E. Litvinenko, Determination of the Class of Validity of Logical Formulas by Directed Exhaustive Search, Cybernetics and Systems Analysis, v.36 n.5, p.652-658, September-October 2000
J. F. Baldwin , T. Martin , B. Azvine, Soft Computing for Intelligent Knowledge-based Systems, BT Technology Journal, v.16 n.3, p.165-179, July 1998
T. P. Dobry , A. M. Despain , Y. N. Patt, Performance studies of a Prolog machine architecture, ACM SIGARCH Computer Architecture News, v.13 n.3, p.180-190, June 1985
Alexander Lyaletski, Sequent forms of Herbrand theorem and their applications, Annals of Mathematics and Artificial Intelligence, v.46 n.1-2, p.191-230, February 2006
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
Enrico Pontelli , Gopal Gupta, Parallel symbolic computation in ACE, Annals of Mathematics and Artificial Intelligence, v.21 n.2-4, p.359-395, 1997
Glenn Shafer , Peter R. Gillett , Richard Scherl, The logic of events, Annals of Mathematics and Artificial Intelligence, v.28 n.1-4, p.315-389, 2000
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
Dominique Pastre, Strong and weak points of the MUSCADET theorem prover - examples from CASC-JC, AI Communications, v.15 n.2,3, p.147-160, August 2002
Henning Christiansen , Davide Martinenghi, On Simplification of Database Integrity Constraints, Fundamenta Informaticae, v.71 n.4, p.371-417, December 2006
Norihiro Kamide, Foundations of Paraconsistent Resolution, Fundamenta Informaticae, v.71 n.4, p.419-441, December 2006
Stephan Schulz, E - a brainiac theorem prover, AI Communications, v.15 n.2,3, p.111-126, August 2002
V. A. Volkov, Declarative Representation of Algorithms of Completion by Critical Pairs, Cybernetics and Systems Analysis, v.37 n.6, p.795-799, November-December 2001
Yukihiro Morita , Haruo Yokota , Kenji Nishida , Hidenori Itoh, Retrieval-By-Unification Operation on a Relational Knowledge Base, Proceedings of the 12th International Conference on Very Large Data Bases, p.52-59, August 25-28, 1986
David Chenho Kung, A Temporal Framework for Database Specification and Verification, Proceedings of the 10th International Conference on Very Large Data Bases, p.91-99, August 27-31, 1984
Louiqa Raschid , Stanley Y. W. Su, A Parallel Processing Strategy for Evaluating Recursive Queries, Proceedings of the 12th International Conference on Very Large Data Bases, p.412-419, August 25-28, 1986
N. Peltier, Representing and Building Models for Decidable Subclasses of Equational Clausal Logic, Journal of Automated Reasoning, v.33 n.2, p.133-170, September 2004
Andrew Davison, 15th July 1972: a significant moment for logic programming, ACM SIGPLAN Notices, v.28 n.4, p.58-60, April 1993
Adid Jazaa, Toward better software automation, ACM SIGSOFT Software Engineering Notes, v.20 n.1, p.79-84, Jan. 1995
Giuseppe Cattaneo , Vincenzo Loia, A common-LISP implementation of an extended Prolog system, ACM SIGPLAN Notices, v.23 n.4, p.87-102, April, 1988
J. N. Hooker, Inference Duality as a Basis for Sensitivity Analysis, Constraints, v.4 n.2, p.101-112, May 1999
Carsten Sinz , Andreas Kaiser , Wolfgang Küchlin, Formal methods for the validation of automotive product configuration data, Artificial Intelligence for Engineering Design, Analysis and Manufacturing, v.17 n.1, p.75-97, January 2003
Maribel Fernández, Type assignment and termination of interaction nets, Mathematical Structures in Computer Science, v.8 n.6, p.593-636, December 1998
A. Glebov , S. Gavrilov , V. Zolotov , Chanhee Oh , R. Panda , M. Becer, False-Noise Analysis for Domino Circuits, Proceedings of the conference on Design, automation and test in Europe, p.20784, February 16-20, 2004
Jacques Cohen, A tribute to Alain Colmerauer, Theory and Practice of Logic Programming, v.1 n.6, p.637-646, November 2001
Dolph Ulrich, A Legacy Recalled and a Tradition Continued, Journal of Automated Reasoning, v.27 n.2, p.97-122, August 2001
Yi-Dong Shen , Li-Yan Yuan , Jia-Huai You, SLT-Resolution for the Well-Founded Semantics, Journal of Automated Reasoning, v.28 n.1, p.53-97, January 2002
J. N. Hooker , G. Rago , V. Chandru , A. Shrivastava, Partial Instantiation Methods for Inference in First-Order Logic, Journal of Automated Reasoning, v.28 n.4, p.371-396, May 2002
Wolfgang Kuuml;chlin , Carsten Sinz, Proving Consistency Assertions for Automotive Product Data Management, Journal of Automated Reasoning, v.24 n.1-2, p.145-163, February 2000
Eugene Goldberg, Proving Unsatisfiability of CNFs Locally, Journal of Automated Reasoning, v.28 n.4, p.417-434, May 2002
Peter Van Roy , Per Brand , Denys Duchier , Seif Haridi , Christian Schulte , Martin Henz, Logic programming in the context of multiparadigm programming: the Oz experience, Theory and Practice of Logic Programming, v.3 n.6, p.717-763, November 2003
Yi Shang , Benjamin W. Wah, A Discrete Lagrangian-Based Global-SearchMethod for Solving Satisfiability Problems, Journal of Global Optimization, v.12 n.1, p.61-99, January 1998
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
Jürgen Giesl, Induction Proofs with Partial Functions, Journal of Automated Reasoning, v.26 n.1, p.1-49, January 2001
J. Barklund, Efficient interpretation of Prolog programs, ACM SIGPLAN Notices, v.22 n.7, p.132-137, July 1987
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
Patricia M. Hill , Roberto Bagnara , Enea Zaffanella, Soundness, idempotence and commutativity of set-sharing, Theory and Practice of Logic Programming, v.2 n.2, p.155-201, March 2002
Minds and Machines staff, Book Reviews, Minds and Machines, v.7 n.2, p.289-320, May 1997
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
Patrik Jansson , Johan Jeuring, Polytypic unification, Journal of Functional Programming, v.8 n.5, p.527-536, September 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
Kevin B. Korb, The Frame Problem: An AI Fairy Tale, Minds and Machines, v.8 n.3, p.317-351, August 1998
Max Moser , Ortrun Ibens , Reinhold Letz , Joachim Steinbach , Christoph Goller , Johann Schumann , Klaus Mayr, SETHEO and E-SETHEO - The CADE-13 Systems, Journal of Automated Reasoning, v.18 n.2, p.237-246, 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
Paliath Narendran , Friedrich Otto, Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories, Journal of Automated Reasoning, v.19 n.1, p.87-115, August 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
Renate A. Schmidt, Decidability by Resolution for Propositional Modal Logics, Journal of Automated Reasoning, v.22 n.4, p.379-396, May 1999
K. Hörwein, Structuring Resolution Proofs by Introducing New Lemmata, Journal of Automated Reasoning, v.19 n.2, p.173-203, October 1997
David A. Plaisted , Yunshan Zhu, Ordered Semantic Hyper-Linking, Journal of Automated Reasoning, v.25 n.3, p.167-217, October 2000
Conor McBride, First-order unification by structural recursion, Journal of Functional Programming, v.13 n.6, p.1061-1075, November 2003
E. F. Storm , R. H. Vaughan, Vulcan: a string handling language with dynamic storage control, Proceedings of the November 17-19, 1970, fall joint computer conference, November 17-19, 1970, Houston, Texas
Roman Gershman , Maya Koifman , Ofer Strichman, An approach for extracting a small unsatisfiable core, Formal Methods in System Design, v.33 n.1-3, p.1-27, December 2008
Benjamín Callejas Bedregal, A normal form which preserves tautologies and contradictions in a class of fuzzy logics, Journal of Algorithms, v.62 n.3-4, p.135-147, July, 2007
Chih-Chun Lee , Jie-Hong R. Jiang , Chung-Yang (Ric) Huang , Alan Mishchenko, Scalable exploration of functional dependency by interpolation and incremental SAT solving, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
J. Montero , D. Gómez , H. Bustince, On the relevance of some families of fuzzy sets, Fuzzy Sets and Systems, v.158 n.22, p.2429-2442, November, 2007
Martin Sulzmann , Peter j. Stuckey, Hm(x) type inference is clp(x) solving, Journal of Functional Programming, v.18 n.2, p.251-283, March 2008
Ruei-Rung Lee , Jie-Hong R. Jiang , Wei-Lun Hung, Bi-decomposing large Boolean functions via interpolation and satisfiability solving, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California
Nicolas Peltier, A Resolution Calculus with Shared Literals, Fundamenta Informaticae, v.76 n.4, p.449-480, December 2007
J. Timmis , A. Hone , T. Stibor , E. Clark, Theoretical advances in artificial immune systems, Theoretical Computer Science, v.403 n.1, p.11-32, August, 2008
Zhaohui Luo, Coercions in a polymorphic type system, Mathematical Structures in Computer Science, v.18 n.4, p.729-751, August 2008
Jakob Nordström , Johan Håstad, Towards an optimal separation of space and length in resolution, Proceedings of the 40th annual ACM symposium on Theory of computing, May 17-20, 2008, Victoria, British Columbia, Canada
R. T. Chien , P. B. Maggs , F. A. Stahl, New directions in legal information processing, Proceedings of the November 16-18, 1971, fall joint computer conference, November 16-18, 1971, Las Vegas, Nevada
Khalil Djelloul , Thi-bich-hanh Dao , Thom FrÜhwirth, Theory of finite or infinite trees revisited, Theory and Practice of Logic Programming, v.8 n.4, p.431-489, July 2008
Daan Leijen, HMF: simple type inference for first-class polymorphism, ACM SIGPLAN Notices, v.43 n.9, September 2008
George W. Ernst , Allen Newell, Some issues of representation in a general problem solver, Proceedings of the April 18-20, 1967, spring joint computer conference, April 18-20, 1967, Atlantic City, New Jersey
Robert Anderson, Completeness results for e-resolution, Proceedings of the May 5-7, 1970, spring joint computer conference, May 05-07, 1970, Atlantic City, New Jersey
K. Biss , R. Chien , F. Stahl, R2: a natural language question-answering system, Proceedings of the May 18-20, 1971, spring joint computer conference, May 18-20, 1971, Atlantic City, New Jersey
Magnus Björk, First Order Stålmarck, Journal of Automated Reasoning, v.42 n.1, p.99-122, January 2009
Anbulagan Anbulagan , Duc Nghia Pham , John Slaney , Abdul Sattar, Old resolution meets modern SLS, Proceedings of the 20th national conference on Artificial intelligence, p.354-359, July 09-13, 2005, Pittsburgh, Pennsylvania
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
Matthias Klusch , Frank Kaufer, WSMO-MX: A hybrid Semantic Web service matchmaker, Web Intelligence and Agent Systems, v.7 n.1, p.23-42, January 2009
John C. Mitchell , Arnab Roy , Mukund Sundararajan, An Automated Approach for Proving PCL Invariants, Electronic Notes in Theoretical Computer Science (ENTCS), 234, p.93-113, March, 2009
Jurriaan Hage , Bastiaan Heeren, Strategies for Solving Constraints in Type and Effect Systems, Electronic Notes in Theoretical Computer Science (ENTCS), 236, p.163-183, April, 2009
Syrine Tlili , Mourad Debbabi, Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code, Journal of Automated Reasoning, v.42 n.2-4, p.265-300, April 2009
Pascual Julián-Iranzo , Clemente Rubio-Manzano , Juan Gallardo-Casero, Bousi~Prolog: a Prolog Extension Language for Flexible Query Answering, Electronic Notes in Theoretical Computer Science (ENTCS), 248, p.131-147, August, 2009
Enn Tyugu, Algorithms and Architectures of Artificial Intelligence, Proceeding of the 2007 conference on Algorithms and Architectures of Artificial Intelligence, p.1-171, June 09, 2007
K. Subramani, Optimal Length Resolution Refutations of Difference Constraint Systems, Journal of Automated Reasoning, v.43 n.2, p.121-137, August 2009
Guillaume Burel , Gilles Dowek, How can we prove that a proof search method is not an instance of another?, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, August 02-02, 2009, Montreal, Quebec, Canada
Igor Stéphan, Boolean Propagation Based on Literals for Quantified Boolean Formulae, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.452-456, May 22, 2006
Matti Järvisalo , Tommi Junttila, Limitations of restricted branching in clause learning, Constraints, v.14 n.3, p.325-356, September 2009
Steffen Hölldobler , Eldar Karabaev , Olga Skvortsova, FLUCAP: a heuristic search planner for first-order MDPs, Journal of Artificial Intelligence Research, v.27 n.1, p.419-439, September 2006
Peter Idestam-Almquist, Generalization of clauses under implication, Journal of Artificial Intelligence Research, v.3 n.1, p.467-489, June 1995
Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, Clause/term resolution and learning in the evaluation of quantified Boolean formulas, Journal of Artificial Intelligence Research, v.26 n.1, p.371-416, May 2006
L. Wos, Automated reasoning: real uses and potential uses, Proceedings of the Eighth international joint conference on Artificial intelligence, p.867-876, August 08-12, 1983, Karlsruhe, West Germany
Christoph Walther, A many-sorted calculus based on resolution and paramodulation, Proceedings of the Eighth international joint conference on Artificial intelligence, p.882-891, August 08-12, 1983, Karlsruhe, West Germany
Luis Farinas-del-Cerro, Temporal reasoning and termination of programs, Proceedings of the Eighth international joint conference on Artificial intelligence, p.926-929, August 08-12, 1983, Karlsruhe, West Germany
Wolfgang Schonfeld, Prolog extensions based on tableau calculus, Proceedings of the 9th international joint conference on Artificial intelligence, p.730-732, August 18-23, 1985, Los Angeles, California
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
Kenneth M. Kahn, Uniform: a language based upon unification which unifies (much of) LISP, Prolog, and Act 1, Proceedings of the 7th international joint conference on Artificial intelligence, p.933-939, August 24-28, 1981, Vancouver, BC, Canada
Vincent J. Digricoli , James J. Lu , V. S. Subrahmanian, And-Or graphs applied to RUE resolution, Proceedings of the 11th international joint conference on Artificial intelligence, p.354-358, August 20-25, 1989, Detroit, Michigan
Dan Benanav, Recognizing unnecessary inference, Proceedings of the 11th international joint conference on Artificial intelligence, p.366-371, August 20-25, 1989, Detroit, Michigan
Parag Singla , Pedro Domingos, Lifted first-order belief propagation, Proceedings of the 23rd national conference on Artificial intelligence, p.1094-1099, July 13-17, 2008, Chicago, Illinois
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
D. Goossens, The conceptual calculus for automatic program understanding, Proceedings of the 7th international joint conference on Artificial intelligence, p.992-997, August 24-28, 1981, Vancouver, BC, Canada
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
Vincent J. Digricoli, The management of heuristic search in boolean experiments with RUE resolution, Proceedings of the 9th international joint conference on Artificial intelligence, p.1154-1161, August 18-23, 1985, Los Angeles, California
K. B. Irani , D. G. Shin, A many-sorted resolution based on an extension of a first-order language, Proceedings of the 9th international joint conference on Artificial intelligence, p.1175-1177, August 18-23, 1985, Los Angeles, California
Takahira Yamaguchi , Yoshikazu Tezuka , Osamu Kakusho, Parallel processing of resolution, Proceedings of the 9th international joint conference on Artificial intelligence, p.1178-1180, August 18-23, 1985, Los Angeles, California
Vincent J. Digrigoli, The efficacy of rue resolution experimental results and heuristic theory, Proceedings of the 7th international joint conference on Artificial intelligence, p.539-547, August 24-28, 1981, Vancouver, BC, Canada
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
Timothy M. Lownie, Extending reflective architectures, Proceedings of the 11th international joint conference on Artificial intelligence, p.446-451, August 20-25, 1989, Detroit, Michigan
Dirk Fuchs , Marc Fuchs, Cooperation between top-down and bottom-up theorem provers, Journal of Artificial Intelligence Research, v.10 n.1, p.169-198, January 1999
Hitoshi Ogawa , Tadahiro Kitahashi , Kokichi Tanaka, The theorem prover using a parallel processing system, Proceedings of the 6th international joint conference on Artificial intelligence, p.665-667, August 20-23, 1979, Tokyo, Japan
Hitoshi Ogawa , Hideaki Nanba , Kokichi Tanaka, An active frame for the knowledge representation, Proceedings of the 6th international joint conference on Artificial intelligence, p.668-675, August 20-23, 1979, Tokyo, Japan
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
Robert F. Simmons , Bertram C. Bruce, Some relations between predicate calculus and semantic net representations of discourse, Proceedings of the 2nd international joint conference on Artificial intelligence, p.524-530, September 01-03, 1971, London, England
Shamim A. Naqvi , Lawrence J. Henschen, Synthesizing least fixed point queries into non-recursive iterative programs, Proceedings of the Eighth international joint conference on Artificial intelligence, p.25-28, August 08-12, 1983, Karlsruhe, West Germany
Reinhold Letz, On the polynomial transparency of resolution, Proceedings of the 13th international joint conference on Artifical intelligence, p.123-129, August 28-September 03, 1993, Chambery, France
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
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
W. W. Bledsoe , Robert S. Boyer , William H. Henneman, Computer proofs of limit theorems, Proceedings of the 2nd international joint conference on Artificial intelligence, p.586-600, September 01-03, 1971, London, England
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
Guilherme Bittencourt, In the quest of the missing link, Proceedings of the 15th international joint conference on Artifical intelligence, p.310-315, August 23-29, 1997, Nagoya, Japan
Gilles Audemard , Laurent Simon, GUNSAT: a greedy local search algorithm for unsatisfiability, Proceedings of the 20th international joint conference on Artifical intelligence, p.2256-2261, January 06-12, 2007, Hyderabad, India
Josh D. Tenenberg, Taxonomic reasoning, Proceedings of the 9th international joint conference on Artificial intelligence, p.191-193, August 18-23, 1985, Los Angeles, California
Andrei Voronkov, Strategies in rigid-variable methods, Proceedings of the 15th international joint conference on Artifical intelligence, p.114-119, August 23-29, 1997, Nagoya, Japan
W. W. Bledsoe, Set variables, Proceedings of the 5th international joint conference on Artificial intelligence, p.501-510, August 22-25, 1977, Cambridge, USA
F. M. Brown, A theorem prover for elementary set theory, Proceedings of the 5th international joint conference on Artificial intelligence, p.534-540, August 22-25, 1977, Cambridge, USA
Ake Hansson , Sten-Ake Tarnlund, A natural programming calculus, Proceedings of the 6th international joint conference on Artificial intelligence, p.348-355, August 20-23, 1979, Tokyo, Japan
Charles Kellogg , Philip Klahr , Larry Travis, Deductive methods for large data bases, Proceedings of the 5th international joint conference on Artificial intelligence, p.203-209, 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
S. D. Litvintchouk , V. R. Pratt, A proof-checker for dynamic logic, Proceedings of the 5th international joint conference on Artificial intelligence, p.552-558, 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
Jack Minker , Daniel H. Fishman , James R. McSkimin, The Q* algorithm: a search strategy for a deductive question-answering system, Proceedings of the 3rd international joint conference on Artificial intelligence, p.31-40, August 20-23, 1973, Stanford, USA
J. P. Jouannaud , Y. Kodratoff, Characterization of a class of functions synthesized from examples by a summers like method using a "B.M.W." matching technique, Proceedings of the 6th international joint conference on Artificial intelligence, p.440-447, August 20-23, 1979, Tokyo, Japan
Josh D. Tenenberg, Preserving consistency across abstraction mappings, Proceedings of the 10th international joint conference on Artificial intelligence, p.1011-1014, August 23-28, 1987, Milan, Italy
Raymond Reiter, A semantically guided deductive system for automatic theorem-proving, Proceedings of the 3rd international joint conference on Artificial intelligence, p.41-46, August 20-23, 1973, Stanford, USA
David Gelperin, Deletion-directed search in resolution-based proof procedures, Proceedings of the 3rd international joint conference on Artificial intelligence, p.47-50, August 20-23, 1973, Stanford, USA
Cordell Green, Application of theorem proving to problem solving, Proceedings of the 1st international joint conference on Artificial intelligence, p.219-239, May 07-09, 1969, Washington, DC
William I. Bullers , Shimon Y. Nof , Andrew B. Whinston, A logic representation of manufacturing control, Proceedings of the 6th international joint conference on Artificial intelligence, p.117-119, August 20-23, 1979, Tokyo, Japan
Richard J. Waldinger , Richard C. T. Lee, PROW: a step toward automatic program writing, Proceedings of the 1st international joint conference on Artificial intelligence, p.241-252, May 07-09, 1969, Washington, DC
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
Arthur J. Nevins, An architecture for knowledge based deduction, Proceedings of the 9th international joint conference on Artificial intelligence, p.335-339, August 18-23, 1985, Los Angeles, California
J. R. Slagle , C. L. Chang , R. C. T. Lee, Completeness theorems for semantic resolution in consequence-finding, Proceedings of the 1st international joint conference on Artificial intelligence, p.281-285, May 07-09, 1969, Washington, DC
James B. Morris, E-resolution: extension of resolution to include the equality relation, Proceedings of the 1st international joint conference on Artificial intelligence, p.287-294, May 07-09, 1969, Washington, DC
Alan Bundy, Doing arithmetic with diagrams, Proceedings of the 3rd international joint conference on Artificial intelligence, p.130-138, August 20-23, 1973, Stanford, USA
Gerard P. Hubt, A mechanization of type theory, Proceedings of the 3rd international joint conference on Artificial intelligence, p.139-146, August 20-23, 1973, Stanford, USA
Jared L. Darlington, Automatic program synthesis in second-order logic, Proceedings of the 3rd international joint conference on Artificial intelligence, p.537-542, August 20-23, 1973, Stanford, USA
Zohar Manna , Richard Waldinger, A deductive approach to program synthesis, Proceedings of the 6th international joint conference on Artificial intelligence, p.542-551, August 20-23, 1979, Tokyo, Japan
Harry E. Pople, On the mechanization of abductive logic, Proceedings of the 3rd international joint conference on Artificial intelligence, p.147-152, August 20-23, 1973, Stanford, USA
D. W. Loveland , M. E. Stickel, A hole in goal trees: some guidance from resolution theory, Proceedings of the 3rd international joint conference on Artificial intelligence, p.153-161, August 20-23, 1973, Stanford, USA
Steven Prestwich , Inês Lynce, Refutation by randomised general resolution, Proceedings of the 22nd national conference on Artificial intelligence, p.1667-1670, July 22-26, 2007, Vancouver, British Columbia, Canada
Francis Jeffry Pelletier, The philosophy of automated theorem proving, Proceedings of the 12th international joint conference on Artificial intelligence, p.1039-1045, August 24-30, 1991, Sydney, New South Wales, Australia
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
Pascal Hitzler, A resolution theorem for algebraic domains, Proceedings of the 18th international joint conference on Artificial intelligence, p.1339-1340, August 09-15, 2003, Acapulco, Mexico
Andrei Voronkov, Automated reasoning: past story and new trends, Proceedings of the 18th international joint conference on Artificial intelligence, p.1607-1612, August 09-15, 2003, Acapulco, Mexico
Lifeng He, UNSEARCHMO: eliminating redundant search space on backtracking for forward chaining theorem proving, Proceedings of the 17th international joint conference on Artificial intelligence, p.618-623, August 04-10, 2001, Seattle, WA, USA
Sheila McIlraith , Eyal Amir, Theorem proving with structured theories, Proceedings of the 17th international joint conference on Artificial intelligence, p.624-631, August 04-10, 2001, Seattle, WA, USA
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 A. Kowalski, Logic programming in artificial intelligence, Proceedings of the 12th international joint conference on Artificial intelligence, p.596-603, August 24-30, 1991, Sydney, New South Wales, Australia
Elmar Eder, Consolution and its relation with resolution, Proceedings of the 12th international joint conference on Artificial intelligence, p.132-136, 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
Javier Larrosa , Federico Heras, Resolution in Max-SAT and its relation to local consistency in weighted CSPs, Proceedings of the 19th international joint conference on Artificial intelligence, p.193-198, July 30-August 05, 2005, Edinburgh, Scotland

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Resolution

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Reducibility and completeness


General Terms:
Algorithms, Theory, Verification

Collaborative Colleagues:
J. A. Robinson: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player