Bertrand Russell, Herbrand's Theorem, and the Assignment Statement

While propositional modal logic is a standard tool, first-order modal logic is not. Indeed, it is not generally understood that conventional first-order syntax is insufficiently expressible. In this paper we sketch a natural syntax and semantics for first-order modal logic, and show how it easily copes with well-known problems. And we provide formal tableau proof rules to go with the semantics, rules that are, at least in principle, automatable.

• Type: Conference
• Year: 1998
• Where: AISC
• Authors: Melvin Fitting
• Keywords: AISC 1998, Artificial Intelligence, Conventional First-order Syntax, First-order Modal Logic, Propositional Modal Logic