A Tractable Logic for Molecular Biology

TL;DR

This paper presents a new logical framework for representing and reasoning about protein-protein interactions in molecular biology, enabling dynamic and nonmonotonic reasoning with decidable properties.

Contribution

It introduces a tractable logic that combines first-order reasoning with second-order circumscription for modeling biological interactions.

Findings

Decidable satisfiability and validity in the proposed logic.

Ability to model dynamic changes in protein interactions.

Deduction rules that produce equivalent first-order formulas.

Abstract

We introduce a logic for knowledge representation and reasoning on protein-protein interactions. Modulo a theory, formulas describe protein structures and dynamic changes. They can be composed in order to add or remove static and dynamic observations. A second-order circumscription operator then enables nonmonotonic reasoning on the changes implied by a formula. We introduce deduction rules that produce formulas which are, up to equivalence, in a first-order fragment with decidable satisfiability and validity. Importantly, the rules can produce circumscribed formulas.