Expressing and Verifying Business Contracts with Abductive

Abstract

In this article, we propose to adopt the SCIFF abductive logic
  language to specify business contracts, and show how its proof
  procedures are useful to verify contract execution and fulfilment.
  SCIFF is a declarative language based on abductive logic
  programming, which accommodates forward rules, predicate
  definitions, and constraints over finite domain variables.  Its
  declarative semantics is abductive, and can be related to that of
  deontic operators; its operational specification is the sound and
  complete SCIFF  proof procedure, defined as a set of transition rules,
  which has been implemented and integrated into a reasoning and
  verification tool.  A variation of the SCIFF proof-procedure
  (g-SCIFF) can be used for static verification of contract
  properties.

  We demonstrate the use of the SCIFF language for business contract
  specification and verification, in a concrete scenario.  In order to
  accommodate integration of SCIFF with architectures for business
  contract, we also propose an encoding of SCIFF contract rules in
  RuleML.