Automated Theorem Proving

Automated Theorem Proving

Higher-Order Modal Logic---A Sketch, Automated Deduction in Classical and Non-Classical Logics, Springer Lecture Notes in Artificial Intelligence 1761, pp 23--38, 1998.

Bertrand Russell, Herbrand's theorem, and the assignment statement. In Jacques Calmet and Jan Plaza, editors, Artificial Intelligence and Symbolic Computation, pages 14--28. Springer Lecture Notes in Artificial Intelligence, 1476, 1998.

Herbrand's theorem for a modal logic. Logic and Foundations of Mathematics, 219--225 A. Cantini, E. Casari, and P. Minari, editors, Kluwer Academic Publishers, 1999.

On quantified modal logic, Fundamenta Informaticae, 39:1-5-121,1999.

LeanTaP Revisited. Journal of Logic and Computation, 8:33--47, 1998

A modal Herbrand theorem. Fundamenta Informaticae , 28:101--122, 1996.

A program to compute Gödel-Löb fixpoints. Bulletin EATCS, 58:118--130, 1996.

Tableaus for many-valued modal logic. Studia Logica , 55:63--87, 1995.

Tableaux for logic programming. Journal of Automated Reasoning , 13:175--188, 1994.

coauthored with Wiktor Marek, and Miroslav Truszczynski. The pure logic of necessitation. Journal of Logic and Computation , 2:349--373, 1992.

Destructive modal resolution. Journal of Logic and Computation , 1:83--97, 1990.

First-order modal tableaux. Journal of Automated Reasoning , 4:191--213, 1988.

Intuitionistic resolution. Atti Degli Incontri di Logica Matematica , 4:59--62, 1987.

Resolution for intuitionistic logic. In Zbigniew W. Ras and Maria Zemankova, editors, Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems 1987 , pages 400--407, Amsterdam, 1987. North-Holland.

A tableau system for propositional S5. Notre Dame Journal of Formal Logic , 18:292--294, 1977.

Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic , 13:237--247, 1972.

A tableau proof method admitting the empty domain. Notre Dame Journal of Formal Logic , 12:219--224, 1971.