Logical contingency analysis for domain-specific languages

Patent metadata

Field	Value
Publication number	US-9378195-B2
Application number	US-201313967610-A
Country	US
Kind code	B2
Filing date	Aug 15, 2013
Priority date	Aug 23, 2012
Publication date	Jun 28, 2016
Grant date	Jun 28, 2016

Abstract

Embodiments relate to validating logical statements in code for domain specific languages. An aspect includes parsing logical statements and annotating constraint type logical statements with specific constraint annotations from the logical grammar of the domain specific language. A non-contradiction graph is built using specific constraint annotations constrained to represent cases satisfying the logical statements and is solved to find a case that satisfies the logical statement or prove that no such case exists, thus locating a contradiction. The non-contradiction graph is negated to form a non-tautology graph constrained to represent cases violating the logical statements and the non-tautology graph is solved to find a case that violates the logical statement or prove that no such case exists, thus locating a tautology. A report is provided regarding at least one case satisfying the logical statement and at least one case violating the logical statement whereby the logical statement is validated.

First claim

What is claimed is:

1. A method for validating a set of logical statements in computer readable code for one of a plurality of domain specific languages, comprising:
parsing the logical statements and annotating the logical statements with specific constraint annotations associated with the domain specific language;
building a non-contradiction graph using the specific constraint annotations constrained to represent cases satisfying the logical statements;
solving the non-contradiction graph to find a case that satisfies the logical statement or to prove that no such case exists thus locating a contradiction;
negating the non-contradiction graph to form a non-tautology graph constrained to represent cases violating the logical statements;
solving the non-tautology graph to find a case that violates the logical statement or to prove that no such case exists thus locating a tautology; and
providing a report as to whether there is at least one case that satisfies the logical statement and at least one case that violates the logical statement whereby the logical statement is validated.

2. A method according to claim 1 further comprising, if a contradiction is located, identifying a minimal subset of statements that are necessary to obtain a contradiction.

3. A method according to claim 1 further comprising, if a tautology is located, identifying a minimal subset of statements that are necessary to obtain a tautology.

4. A method according to claim 1 wherein solving comprising using a general theory solver utilizing a combination of specialized solvers for the mathematical theories wherein the type of solver needed is defined by the annotations.

5. A method according to claim 4 wherein specialized solvers are one or more of: an arithmetic solver; a Boolean algebra solver; an order theory solver; a set algebra solver; and/or an equality theory solver.

6. A method according to claim 1 further comprising producing a certificate of contingency that includes a case free of contradiction and tautology, or producing a certificate of contingency that includes a case with contradiction and tautology.

7. A computer program product for validating a logical statement in computer readable code for one of a plurality of domain specific languages, the computer program product comprising:
a non-transitory computer readable storage medium having program code embodied therewith, the program code executable by a processor for:
parsing the logical statements and annotating the logical statements with specific constraint annotations associated with the domain specific language;
building a non-contradiction graph using the specific constraint annotations constrained to represent cases satisfying the logical statements;
solving the non-contradiction graph to find a case that satisfies the logical statement or to prove that no such case exists thus locating a contradiction;
negating the non-contradiction graph to form a non-tautology graph constrained to represent cases violating the logical statements;
solving the non-tautology graph to find a case that violates the logical statement or to prove that no such case exists thus locating a tautology; and
providing a report as to whether there is at least one case that satisfies the logical statement and at least one case that violates the logical statement whereby the logical statement is validated.

8. A computer program product according to claim 7 further comprising, if a contradiction is located, identifying a minimal subset of statements that are necessary to obtain a contradiction.

9. A computer program product according to claim 7 further comprising, if a tautology is located, identifying a minimal subset of statements that are necessary to obtain a tautology.

10. A computer program product according to claim 7 wherein solving comprising using a general theory solver utilizing a combination of specialized solvers for the mathematical theories wherein the type of solver needed is defined by the annotations.

11. A computer program product according to claim 10 wherein specialized solvers are one or more of: an arithmetic solver; a Boolean algebra solver; an order theory solver; a set algebra solver; and/or an equality theory solver.

12. A computer program product according to claim 7 further comprising, producing a certificate of contingency that includes a case free of contradiction and tautology, or producing a certificate of contingency that includes a case with contradiction and tautology.

13. A method for validating a set of logical statements in computer readable code for one of a plurality of domain specific languages, comprising:
parsing the logical statements and annotating the logical statements with specific constraint annotations associated with the domain specific language;
building a first graph using the specific constraint annotations to represent cases satisfying the logical statements;
solving the first graph to find a case that satisfies the logical statement or to prove that no such case exists thus locating a contradiction;
negating, where the first graph is valid, the first graph to form a second graph to represent cases violating the logical statements;
solving the second graph to find a case that violates the logical statement or to prove that no such case exists thus locating a tautology; and
providing a report as to whether there is at least one case that satisfies the logical statement and at least one case that violates the logical statement whereby the logical statement is validated.

14. A method according to claim 13 further comprising, if a contradiction is located, identifying a minimal subset of statements that are necessary to obtain a contradiction.

15. A method according to claim 13 further comprising, if a tautology is located, identifying a minimal subset of statements that are necessary to obtain a tautology.

16. A method according to claim 13 further comprising, producing a certificate of contingency that includes a case free of contradiction and tautology, or producing a certificate of contingency that includes a case with contradiction and tautology.

Assignees

• IBM

Inventors

• Bernelas Jean Michel
• Junker Ulrich
• Kormann Thierry
• Mery Stephane

Classifications

• G06N5/00

  Computing arrangements using knowledge-based models · CPC title

• G06F40/226

  Validation · CPC title

• G06F8/436 Primary

  Semantic checking · CPC title

• G06F16/90332

  Natural language query formulation or dialogue systems · CPC title

• G06F8/43 Primary

  Checking; Contextual analysis · CPC title