Journal of the ACM Bibliography

Selected papers that cite this one

• Robert Anderson and W. W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. Journal of the ACM, 17(3):525-534, July 1970.

• Peter B. Andrews. Resolution with merging. Journal of the ACM, 15(3):367-381, July 1968.

• Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6(6):579-612, December 1996.

• Marco Bellia and M. Eugenia Occhiuto. Suprema of open and closed formulas and their application to resolution. Information and Computation, 117(1):136-150, 15 February 1995.

• W. Bibel and E. Eder. Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution. Journal of the ACM, 44(2):320-344, March 1997.

• Howard A. Blair. The recursion-theoretical complexity of the semantics of predicate logic as a programming language. Information and Control, 54(1/2):25-47, July/August 1982.

• Wray L. Buntine and Hans-Jürgen Bürckert. On solving equations and disequations. Journal of the ACM, 41(4):591-629, July 1994.

• Yair Caro, András Seb\H{o}, and Michael Tarsi. Recognizing greedy structures. Journal of Algorithms, 20(1):137-156, January 1996.

• C. L. Chang. The unit proof and the input proof in theorem proving. Journal of the ACM, 17(4):698-707, October 1970.

• C. L. Chang, R. C. T. Lee, and J. K. Dixon. The specialization of programs by theorem proving. SIAM Journal on Computing, 2(1):7-15, March 1973.

• C. L. Chang and J. R. Slagle. Completeness of linear refutation for theories with equality. Journal of the ACM, 18(1):126-136, January 1971.

• John K. Dixon. Z-resolution: Theorem-proving with compiled axioms. Journal of the ACM, 20(1):127-147, January 1973.

• Gilles Dowek. A complete proof synthesis method for the cube of type systems. Journal of Logic and Computation, 3(3):287-315, June 1993.

• Dominic Duggan and Frederick Bent. Explaining type inference. Science of Computer Programming, 27(1):37-83, July 1996.

• George W. Ernst. Sufficient conditions for the success of GPS. Journal of the ACM, 16(4):517-533, October 1969.

• M. Falaschi, G. Levi, and C. Palamidessi. A synchronization logic: Axiomatics and formal semantics of generalized Horn clauses. Information and Control, 60(1-3):36-69, January/February/March 1984.

• Michael Fisher. A normal form for temporal logics and its applications in theorem-proving and execution. Journal of Logic and Computation, 7(4):429-456, August 1997.

• S. Fleisig, D. Loveland, A. K. Smiley III, and D. L. Yarmush. An implementation of the model elimination proof procedure. Journal of the ACM, 21(1):124-139, January 1974.

• Wan Fokkink. Unification for infinite sets of equations between finite terms. Information Processing Letters, 62(4):183-188, 28 May 1997.

• Jean-Denis Fouks and Jean-Claude Spehner. Meta-resolution: An algorithmic formalisation. Theoretical Computer Science, 166(1-2):147-172, 20 October 1996.

• Merrick L. Furst and Ravi Kannan. Succinct certificates for almost all subset sum problems. SIAM Journal on Computing, 18(3):550-558, June 1989.

• Paola Giannini and Simona Ronchi Della Rocca. A type inference algorithm for a stratified polymorphic type discipline. Information and Computation, 109(1/2):115-173, 15 February/March 1994.

• Éric Grégoire and Pierre Marquis. Novelty in deductive databases. Journal of Logic and Computation, 6(5):683-708, October 1996.

• Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, January 1993.

• Leen Helmink. Resolution and type theory. Science of Computer Programming, 17(1-3):119-138, December 1991.

• Fritz Henglein and Harry G. Mairson. The complexity of type inference for higher-order typed lambda calculi. Journal of Functional Programming, 4(4):435-477, October 1994.

• G. P. Huet. A unification algorithm for typed lambda-calculus. Theoretical Computer Science, 1(1):27-57, June 1975.

• Mark P. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, 5(1):1-35, January 1995.

• Mark P. Jones. First-class polymorphism with type inference. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 483-496, Paris, France, 15-17 January 1997.

• Mark P. Jones. A theory of qualified types. Science of Computer Programming, 22(3):231-256, June 1994.

• Richard B. Kieburtz and David Luckham. Compatibility and complexity of refinements of the resolution principle. SIAM Journal on Computing, 1(4):313-332, December 1972.

• Richard C. T. Lee. Fuzzy logic and the resolution principle. Journal of the ACM, 19(1):109-119, January 1972.

• D. W. Loveland. A simplified format for the model elimination theorem-proving procedure. Journal of the ACM, 16(3):349-363, July 1969.

• D. W. Loveland. A unifying view of some linear Herbrand procedures. Journal of the ACM, 19(2):366-384, April 1972.

• Donald W. Loveland. Mechanical theorem-proving by model elimination. Journal of the ACM, 15(2):236-251, April 1968.

• Ian Mackie. Lilac: a functional programming language based on linear logic. Journal of Functional Programming, 4(4):395-433, October 1994.

• Zohar Manna. Properties of programs and the first-order predicate calculus. Journal of the ACM, 16(2):244-255, April 1969.

• Aart Middeldorp, Satoshi Okui, and Tetsuo Ida. Lazy narrowing: Strong completeness and eager variable elimination. Theoretical Computer Science, 167(1-2):95-130, 30 October 1996.

• Arthur J. Nevins. A human oriented logic for automatic theorem-proving. Journal of the ACM, 21(4):606-621, October 1974.

• H. J. Ohlbach. Semantics-based translation methods for modal logics. Journal of Logic and Computation, 1(5):691-746, October 1990.

• Friedrich Otto, Paliath Narendran, and Daniel J. Dougherty. Equational unification, word unification, and 2nd-order equational unification. Theoretical Computer Science, 198(1-2):1-47, 30 May 1998. Fundamental Study.

• Ross A. Overbeek. A new class of automated theorem-proving algorithms. Journal of the ACM, 21(2):191-200, April 1974.

• Tomasz Pietrzykowski. A complete mechanization of second-order type theory. Journal of the ACM, 20(2):333-365, April 1973.

• J. R. Quinlan and E. B. Hunt. A formal deductive problem-solving system. Journal of the ACM, 15(4):625-646, October 1968.

• Alexander Razborov, Avi Wigderson, and Andrew Yao. Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus. In Proceedings of the Twenty-Ninth Annual ACM Symposium on Theory of Computing, pages 739-748, El Paso, Texas, 4-6 May 1997.

• Raymond Reiter. Two results on ordering for resolution with merging and linear format. Journal of the ACM, 18(4):630-646, October 1971.

• James R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687-697, October 1967.

• James R. Slagle. Interpolation theorems for resolution in lower predicate calculus. Journal of the ACM, 17(3):535-542, July 1970.

• James R. Slagle. Automatic theorem proving with built-in theories including equality, partial ordering, and sets. Journal of the ACM, 19(1):120-135, January 1972.

• Rona B. Stillman. The concept of weak substitution in theorem-proving. Journal of the ACM, 20(4):648-667, October 1973.

• Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 111(2):245-296, June 1994.

• Tanel Tammet. Completeness of resolution for definite answers. Journal of Logic and Computation, 5(4):449-471, August 1995.

• Farn Wang. A temporal logic for real-time partial ordering with named transactions. Theoretical Computer Science, 181(1):195-225, 15 July 1997.

• Trudy Weibel. An order-sorted resolution in theory and practice. Theoretical Computer Science, 185(2):393-410, 20 October 1997.

• Lawrence Wos, George A. Robinson, and Daniel F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM, 12(4):536-541, October 1965.

• Lawrence Wos, George A. Robinson, Daniel F. Carson, and Leon Shalla. The concept of demodulation in theorem proving. Journal of the ACM, 14(4):698-709, October 1967.

• Kwangkeun Yi. An abstract interpretation for estimating uncaught exceptions in Standard ML programs. Science of Computer Programming, 31(1):147-173, May 1998.

Selected references

• Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.

• Joyce Friedman. A semi-decision procedure for the functional calculus. Journal of the ACM, 10(1):1-24, January 1963.

• J. A. Robinson. Theorem-proving on the computer. Journal of the ACM, 10(2):163-174, April 1963.

Shortcuts: