Melvin Fitting

FLAP Journal 2020 Journal Article

Bilattice Basics.

• Melvin Fitting

FLAP Journal 2015 Journal Article

Cut-Free Proof Systems for Geach Logics.

• Melvin Fitting

Prefixed tableaus for modal logics have been around since the early 1970s, and are quite familiar by now. Rather recently it was found that they were dual to nested sequents, which have a complicated history but which also trace back to the 1970’s. Both have provided very natural proof systems for the most common modal logics, including those in the so-called modal cube. In this paper we add some simple machinery to both prefixed tableaus and to nested sequents, producing cut-free proof systems for all logics axiomatized by Geach formulas, that is, by axiom schemes of the form ♦k l X ⊃ m ♦n X. This again provides proof mechanisms for the modal cube, but mechanisms of a different nature than usual. But further, it provides proof mechanisms for an infinite family of modal logics, and does so in a modular way with a clear separation between logical and structural rules. The version of nested sequents presented here has a direct relationship with the formal machinery of [23], and can be thought of as a notational variant of a natural and interesting fragment of what can be handled using that methodology.

TCS Journal 2002 Journal Article

Fixpoint semantics for logic programming a survey

• Melvin Fitting

The variety of semantical approaches that have been invented for logic programs is quite broad, drawing on classical and many-valued logic, lattice theory, game theory, and topology. One source of this richness is the inherent non-monotonicity of its negation, something that does not have close parallels with the machinery of other programming paradigms. Nonetheless, much of the work on logic programming semantics seems to exist side by side with similar work done for imperative and functional programming, with relatively minimal contact between communities. In this paper we summarize one variety of approaches to the semantics of logic programs: that based on fixpoint theory. We do not attempt to cover much beyond this single area, which is already remarkably fruitful. We hope readers will see parallels with, and the divergences from the better known fixpoint treatments developed for other programming methodologies.

TCS Journal 1986 Journal Article

Partial models and logic programming

• Melvin Fitting

Three extensions of the standard Prolog fixpoint semantics are presented (called sat, strong, and weak), using partial models, models which may fail to assign truth values to all formulas. Each of these semantics takes negation and quantification into account. All thee are conservative: they agree with the conventional semantics on pure Horn clause programs. The sat and the strong semantics incorporate the domain closure assumption, but differ on whether to assign a truth value to a classically valid formula some part of which lacks a truth value. The weak semantics is similar to the strong semantics but abandons the domain closure condition, and consequently, all programs give rise to continuous operators in this semantics. For the weak semantics, a sound and complete proof procedure is given, based on semantics tableaus (or equivalently, Gentzen Sequents).