Detecting inconsistencies in semantics of business vocabulary and business rules (SBVR) using many-sorted logic

A system for detecting inconsistencies in Semantics of Business Vocabulary and Business Rules (SBVR) using Many-Sorted Logic, the system comprising:

• a memory storing instructions;
• one or more communication interfaces;
• and
• one or more hardware processors coupled to the memory via the one or more communication interfaces, wherein the one or more hardware processors are configured by the instructions to:
• define a set of rules expressed in SBVR, wherein the set of rules comprises syntactic and semantic ambiguities and inconsistencies, and wherein each of the set of rules facilitate one or more actions based upon a specification of one or more conditions;
• translate the set of SBVR rules into a SBVR eXtensible Markup Language Metadata Interchange (XMI) comprising segregated SBVR vocabulary and rules, wherein the translating is performed by implementing a clustering technique on the set of SBVR rules, wherein the translating comprises generating a plurality of graphical clusters for the segregated SBVR vocabulary to schematically represent an inheritance in the segregated SBVR vocabulary;
• transform the SBVR XMI into one or more Satisfiability Modulo Theories Library (SMT-LIB) formulas using at least one logical structure and semantic of Many-Sorted Logic, wherein the transforming comprises a mapping of each of the segregated SBVR rules into a corresponding SMT-LIB representation using one or more axioms, for capturing a set of existing information in each of the segregated SBVR rules;
• and
• detect, from the one or more SMT-LIB formulas, one or more inconsistencies in semantics of SBVR by using a Satisfiability Modulo Theories (SMT) solver invocation;
• wherein:
• the one or more hardware processors are configured to detect the one or more inconsistencies by extracting, via a Mapping Regions of Constraint sets (MARCO) technique, all minimally unsatisfiable sub-formulas from the one or more SMT-LIB formulas, and wherein the minimally unsatisfiable sub-formulas are minimal set of rules in the one or more SMT-LIB formulas inconsistent with each other;
• and
• the step of extracting all the minimally unsatisfiable sub-formulas facilitate a simultaneous detection of the one or more inconsistencies from the one or more SMT-LIB formulas.