Proof search in the intuitionistic sequent calculus

1. M. J. Beeson. Some applications of Gentzen's proof theory in automated deduction. In P. Schroeder-Heister, editor, Extensions of Logic Programming, Lecture Notes in Computer Science 475, pages 101–156. Springer-Verlag, 1991.

   Google Scholar 

2. G. L. Bellin. Herbrand's theorem for calculi of sequents LK and LJ. In D. Prawitz, editor, Proceedings of the Third Scandinavian Logic Symposium, 1980.

   Google Scholar 

3. W.W. Bledsoe and P. Bruell. A man-machine theorem-proving system. In Advance Papers of Third International Joint Conference on Artificial Intelligence. W.W. Bledsoe, 1974.

   Google Scholar 

4. K. A. Bowen. Programming with full Jirst-order logic. In J. E. Hayes, D. Michie, and Y.-H. Pao, editors, Machine Intelligence 10, pages 421–440. Halsted Press, 1982.

   Google Scholar 

5. R. L. Constable, et al., Implementing Mathematics with the Nuprl. Prentice-Hall, New Jersey, 1986.

   Google Scholar 

6. A. Felty and D. Miller. Specifying theorem provers in a higher-order logic programming language. In E. Lusk and R. Overbeek, editors, Ninth International Conference on Automated Deduction, Lecture Notes in Computer Science 310, pages 61–80, Argonne, Illinois, May 1988.

   Google Scholar 

7. M. Fitting, First-Order Logic and Automated Theorem Proving. Springer-Verlag, 1990.

   Google Scholar 

8. K. Gödel. An interpretation of the intuitionistic propositional calculus. In S. Feferman, editor, Kurt Gödel: Collected Works Vol. I, pages 301–303. Oxford University Press, 1986.

   Google Scholar 

9. K. Gödel. On intuitionistic arithmetic and number theory. In S. Feferman, editor, Kurt Gödel: Collected Works Vol. 1, pages 287–295. Oxford University Press, 1986.

   Google Scholar 

10. J. Herbrand. Investigations in proof theory. In J. van Heijenoort, editor, From Frege to Gödel: A Source Book of Mathematical Logic, pages 525–581. Harvard University Press, Cambridge, Mass., 1967.

    Google Scholar 

11. J. Ketonen and R. Weyhrauch. A decidable fragment of predicate calculus. The Journal of Theoretical Computer Science, 32:297–307, 1984.

    Google Scholar 

12. S. C. Kleene. Introduction to Metamathematics. North-Holland, Amsterdam, 1952.

    Google Scholar 

13. S. C. Kleene. Permutability of inferences in Gentzen's calculi LK and LJ. Memoirs of the AMS, 10, 1952.

    Google Scholar 

14. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

    Google Scholar 

15. G. Mints. Gentzen-type systems and resolution rules, Part I: Propositional logic. In P. Martin-Löf and G. Mints, editors, COLOG-88, Lecture Notes in Computer Science 417, pages 198–231. Springer-Verlag, 1988.

    Google Scholar 

16. G. E. Mints. Analog of Herbrand's theorem for non-prenex formulas of constructive predicate calculus. In Studies in constructive mathematics and mathematical logic, I. Steklov Mathematical Institute Seminars in Mathematics, 1969.

    Google Scholar 

17. G. Nadathur and D. Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777–814, 1990.

    Google Scholar 

18. D. J. Pym and L. A. Wallen. Investigations into proof-search in a system of first-order dependent function types. In M. E. Stickel, editor, Tenth Conference on Automated Deduction, Lecture Notes in Computer Science 449, pages 236–250. Springer-Verlag, 1990.

    Google Scholar 

19. M. E. Szabo, editor. The Collected Papers of Gerhard Gentzen. North-Holland, 1969.

    Google Scholar 

20. L. A. Wallen. Automated Proof Search in Non-Classical Logics. MIT Press, 1990.

    Google Scholar 

Download references