Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification

1. A. Beltyukov. Decidability of the universal theory of natural numbers with addition and divisibility (in Russian). Zapiski Nauchnyh Seminarov LOMI, 60:15–28, 1976. English translation in: Journal of Soviet Mathematics.

   Google Scholar 

2. A. Degtyarev, Yu. Matiyasevich, and A. Voronkov. Simultaneous rigid E-unification and related algorithmic problems. In LICS'96, page 11, 1996.

   Google Scholar 

3. A. Degtyarev and A. Voronkov. Equality elimination for semantic tableaux. UP-MAIL Technical Report 90, Uppsala University, Computing Science Department, December 1994.

   Google Scholar 

4. A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, Computing Science Department, May 1995. To appear in Theoretical Computer Science.

   Google Scholar 

5. A. Degtyarev and A. Voronkov. Reduction of second-order unification to simultaneous rigid E-unification. UPMAIL Technical Report 109, Uppsala University, Computing Science Department, June 1995.

   Google Scholar 

6. A. Degtyarev and A. Voronkov. A new procedural interpretation of Horn clauses with equality. In Leon Sterling, editor, Proceedings of the Twelfth International Conference on Logic Programming, pages 565–579. The MIT Press, 1995.

   Google Scholar 

7. A. Degtyarev and A. Voronkov. General connections via equality elimination. In M. De Glas and Z. Pawlak, editors, Second World Conference on the Fundamentals of Artificial Intelligence (WOCFAI-95), pages 109–120, Paris, July 1995. Angkor.

   Google Scholar 

8. A. Degtyarev and A. Voronkov. Equality elimination for the inverse method and extension procedures. In C.S. Mellish, editor, Proc. International Joint Conference on Artificial Intelligence (IJCAI), volume 1, pages 342–347, Montréal, August 1995.

   Google Scholar 

9. A. Degtyarev and A. Voronkov. Skolemization and decidability problems for fragments of intuitionistic logic. Submitted, 10 pages, 1996.

   Google Scholar 

10. M. Fitting. First Order Logic and Automated Theorem Proving. Springer Verlag, New York, 1990.

    Google Scholar 

11. J.H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification: Equational matings. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338–346. IEEE Computer Society Press, 1987.

    Google Scholar 

12. S. Kanger. A simplified proof method for elementary logic. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 364–371. Springer Verlag, 1983. Originally appeared in 1963.

    Google Scholar 

13. R.C.T. Lee and C.L. Chang. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.

    Google Scholar 

14. V. Lifschitz. The decidability problem for some constructive theories of equality (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4:78–85, 1967.

    Google Scholar 

15. D.W. Loveland. Automated Theorem Proving: a Logical Basis. North Holland, 1978.

    Google Scholar 

16. S.Yu. Maslov. An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. In J.Siekmann and G.Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 2, pages 48–54. Springer Verlag, 1983.

    Google Scholar 

17. S.Yu. Maslov. An invertible sequential variant of constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4, 1967. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, p.36–42.

    Google Scholar 

18. V. A. Matulis. On variants of classical predicate calculus with the unique deduction tree (in Russian). Soviet Mathematical Doklady, 148:768–770, 1963.

    Google Scholar 

19. G.E. Mints. Collecting terms in the quantifier rules of the constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4:78–85, 1967.

    Google Scholar 

20. V.P. Orevkov. Solvable classes of pseudo-prenex formulas (in Russian). Zapiski Nauchnyh Seminarov LOMI, 60:109–170, 1976. English translation in: Journal of Soviet Mathematics.

    Google Scholar 

21. D.A. Plaisted. Special cases and substitutes for rigid E-unification. Technical Report MPI-I-95-2-010, Max-Planck-Institut für Informatik, November 1995.

    Google Scholar 

22. G. Plotkin. Building-in equational theories. In Meltzer and Michie, editors, Machine Intelligence, volume 7, pages 73–90. Edinburgh University Press, Edinburgh, 1972.

    Google Scholar 

23. G. Robinson and L.T. Wos. Paramodulation and theorem-proving in first order theories with equality. In Meltzer and Michie, editors, Machine Intelligence, volume 4, pages 135–150. Edinburgh University Press, Edinburgh, 1969.

    Google Scholar 

24. D. Sahlin, T. Franzén, and S. Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2(5):619–656, 1992.

    Google Scholar 

25. N. Shankar. Proof search in the intuitionistic sequent calculus. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 522–536, Saratoga Springs, NY, USA, June 1992. Springer Verlag.

    Google Scholar 

26. T. Tammet. A resolution theorem prover for intuitionistic logic. This volume.

    Google Scholar 

27. M. Veanes. Undecidability proofs of simultaneous rigid E-unification. Upmail technical report, Uppsala University, Computing Science Department, 1996. To appear.

    Google Scholar 

28. P.J. Voda and J. Komara. On Herbrand skeletons. Technical report, Institute of Informatics, Comenius University Bratislava, July 1995.

    Google Scholar 

29. A. Voronkov. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 648–662, Saratoga Springs, NY, USA, June 1992. Springer Verlag.

    Google Scholar 

30. A. Voronkov. Proof-search in intuitionistic logic based on the constraint satisfaction. UPMAIL Technical Report 120, Uppsala University, Computing Science Department, January 1996.

    Google Scholar 

31. A. Voronkov. On proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-Unification. UPMAIL Technical Report 121, Uppsala University, Computing Science Department, January 1996.

    Google Scholar 

Download references