Formal Theorem Proving

Tableaus and Dual Tableaus, In Ewa Orlowska on Relational Methods in Logic and Computer Science. edited by Joanna Golinska-Pilarek and Michal Zawidzki. Vol. 17. Outstanding Contributions to Logic 5. Cham, Switzerland: Springer, 2018. pp. 105-128.

Cut-Free proof systems for Geach logics, The IfCoLog Journal of Logics and their Applications. 2(2), 17 - 64, 2015.

Nested Sequents for Intuitionistic Logic, Notre Dame Journal of Formal Logic, 55(1):41-61, 2014.

Prefixed tableaus and nested sequents. Annals of Pure and Applied Logic, 163:291-313, 2012.

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.

Introduction, in Handbook of Tableau Methods, Marcello D'Agostino, Dov M. Gabbay, Reiner Hähnle, Joachim Posegga editors, Kluwer, 1999, pp. 1--43.

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.

[Go home]