US 12,254,082 B1
Using first-order theories of boolean algebras to provide safe artificial intelligence (AI) systems and a novel software specification logic
Ohad Asor, Triesen (LI)
Assigned to IDNI AG, Triesen (LI)
Filed by IDNI AG, Triesen (LI)
Filed on Jul. 17, 2024, as Appl. No. 18/776,245.
Claims priority of provisional application 63/667,692, filed on Jul. 3, 2024.
Claims priority of provisional application 63/564,501, filed on Mar. 12, 2024.
Int. Cl. G06F 21/52 (2013.01)
CPC G06F 21/52 (2013.01) 20 Claims
OG exemplary drawing
 
1. A method of symbolic artificial intelligence, performed at a computing device having one or more processors and memory storing one or more programs configured for execution by the one or more processors, the method comprising:
identifying an atomless Boolean Algebra B and a first-order language (logic) of Boolean Algebras, the language having constant symbols 0, 1, and extended with a plurality of additional constant symbols, each constant symbol uniquely interpreted as a respective element of B;
accessing an expression written in the extended first-order language, wherein the expression has one or more logical quantifiers and specifies whether to accept a software update on the computing device;
selecting an innermost quantifier having a quantified variable x, and, when the innermost quantifier is not an existential quantifier, converting the expression so that the innermost quantifier is an existential quantifier;
identifying a subexpression f, of the expression, to which the innermost quantifier applies;
viewing the subexpression f as in disjunctive normal form having one or more DNF clauses ci, i ϵ I, each DNF clause comprising a conjunction of one or more literals, each literal is either (a) a positive literal pij(x)=0, j ϵ J1, or (b) a negative literal nij(x)≠0, j ϵ J2;
for each DNF clause ci:
forming a single substitute positive literal pi(x)=0 by either (a) combining all positive literals pij(x)=0, j ϵ J1, for the respective DNF clause into a single positive literal ∪jϵJ1 pij(x)=0 when there is at least one positive literal or (b) specifying the single substitute positive literal as 0=0 when there is not at least one positive literal;
constructing a respective output clause of the form:

OG Complex Work Unit Math
constructing a modified expression by replacing the innermost quantifier and the subexpression f with a disjunction of the DNF output clauses, thereby eliminating the innermost quantifier; and
computing a truth value t for the modified expression and, when t is true, installing the software update on the computing device.