Journal Paper

Particular reasoning enables the deductive proof of existential properties, such as the satisfiability/consistency of a set of formulas. In this work, we consider particular reasoning in the context of a theory of a given logic. The logic is presented by a semantic constraint specification. From this specification, we induce a particular calculus for the logic at hand. In this calculus we define what is a particular derivation in the context of a theory and show how to extract a model of the theory that satisfies the assertions within the derivation. We demonstrate that the induced particular calculus is both sound and complete with regard to the intended semantics. Our results are applicable to logics with a strong finite model property, including classical, intuitionistic, certain modal logics, and Nelson’s N4 logic, among others.