Method of automated proving for unrestricted first-order logic

US6424962B1 · kind B1 · utility

Assignee

• Bull S.A. · FR

Inventor

• Jean-Paul Billon · Bron, FR

Key dates

• Filing date: Sep 19, 1997
• Grant date: Jul 23, 2002
• Expiry date: Jan 2, 2021

Classification

• Technology area (CPC G): Physics
• CPC primary: G06N5/01
• WIPO field: Computer technology
• WIPO sector: Electrical engineering

Abstract

A method of automated proving for unrestricted first-logic to test the satisfiability of clause sets describing an industrial system which applies the instance generation rule where &PSgr; is a term, &sgr; a substitution and &PSgr;&sgr; an instance of &PSgr; yielded by the substitution &sgr;, and is characterized in that, instance subtraction is defined as the substraction of the instance &PSgr;&sgr; from &PSgr; resulting in a generalized term which is a triplet <&PSgr;, &sgr;, &Lgr;> where &Lgr; is a finite set of standard substitutions {&lgr;1, . . . , &lgr;n} and defined byGE(<&PSgr;, &sgr;, &Lgr;>)=GE(&PSgr;&sgr;)&#8722;GE({&PSgr;&lgr;1, . . . , &PSgr;&lgr;n})the method further applies an instance subtraction combined with said instance generation rule to get an instance extraction rule defined by(IE)&Sgr;&#8594;(&Sgr;&#8722;{&PSgr;<&sgr;,&Lgr;>})&#8746;{&PSgr;<&sgr;&mgr;,&Lgr;*&sgr;&mgr;>, &PSgr;<&sgr;,&Lgr;&#8746;{&sgr;&mgr;}>)where &Sgr; is a set of clauses and &mgr; is a substitution valid for the generalized term &PSgr;<&sgr;, &Lgr;>, whereby the set &Sgr; can be proven unsatisfiable.