Franci, Math Consultant™ : Description

Franci's current version, as of May 17, 2002, is 0.4.0.0 .
Franci's stable version, as of May 17, 2002, is 0.4.0.0 .

Main changes from 0.3.9.9 to 0.4.0.0:

Changes to Franci script language™: Multiplication · and multiplicative inverse ^-1.

Other changes:

• Franci now automatically solves linear equations in one variable. Automatic typing responds to such solutions.
• The inference engine is somewhat more careful in its choice of test cases.

Franci can use a script written in Franci script language™ that defines a mathematical situation, and generate a Franci logfile™ that documents her analysis of the situation. If so requested, the Franci logfile™ can document her analysis in a humanly verifiable fashion.

Franci script language™ specifications

• If a script line starts (after whitespace) with // , then Franci interprets this as a C++ comment. She ignores the entire script line, silently.

• start logfile
• Starts a logfile, named "Franci.txt".
• end logfile
• Ends the current logfile.
• clean logfile
• Cleans the logfile. If the logfile is open, it will be ended first.
• Currently, Franci scans for test cases whose work is invalidated by later work, and replaces them with "...".
• evaluate ___
• Franci evaluates an expression. She explains the steps she takes to get her answer.
• If you don't want Franci to explain the steps: Evaluate ___
• evaluate situation
• Franci evaluates the current situation (specified earlier). The evaluated situation replaces the initial situation. Franci does not look for lemmas, but does explain the steps she takes to get her answer.
• If you don't want Franci to explain the steps in detail: Evaluate situation
• new variable: THEREIS __,__,...,___ IN ____
• Example: new variable: THEREIS X_1,Y2,Z IN TruthValues
• The list between THEREIS and IN all must be potential variable names.
• The single argument after IN must denote a set.
• no-log version: New Variable: THEREIS __,__,...,___ IN ___
• new situation
• Franci forgets the current situation entirely.
• no more variables
• Franci is informed that she is not to improvise any more variables.
• This command also turns the "new variable:" command into a run-time error.
• constraint: ____
• Franci checks that the expression is interpretable as true or false. If it is, she improvises any needed variables (if allowed to), and adds the constraint to the current situation definition if all required improvisations succeeded. Franci records the constraint.
• If you don't want Franci to record the constraint: Constraint: ____
• what if: ____
• Franci checks that the expression is interpretable as true or false. This expression must not require any new variables to be improvised. If the expression is allowable, Franci analyzes the current situation under the assumption that the expression specified by what if: is true. Franci will look for lemmas, and incorporate them into her analysis. Franci explains what steps she is taking to get both the lemmas, and her final answer.
• If you don't want Franci to explain the lemmas in detail: What if ___
• what is ___
• Franci interprets this as "evaluate ___".
• Franci interprets "What is ___" as "Evaluate ___"

• ( ) [ ] { } , ;
• ASCII space, or the start of the script line

• TRUE, FALSE, UNKNOWN, CONTRADICTION
• TRUE, FALSE, UNKNOWN are to be interpreted according to their usual mathematical usage.
• CONTRADICTION is to be interpreted as: 'not possibly true' AND 'not possibly false'.
• positive integer strings: sequences of digits 0..9
• Examples: 0, 23, 123456789232425 (yes, this one is larger than the maximum of a 32-bit unsigned long.)
• The only limits on the size of an explicitly represented integer are RAM, file size, and human tolerance for large integers.
• Franci also accepts negative integers, such as -124.
• potential variable names: sequences of letters a..z, A..Z, digits 0..9, or the character _, not starting with a digit.
• Examples: AB, A_2, a2_XyZ, _23A, _A34
• This is not a potential variable name: 123AB_3
• Franci parses this as: 123 AB_3
• Various reserved set and class names
• TruthValues: the set {TRUE, FALSE, UNKNOWN, CONTRADICTION}.
• _Z_, _Q_, _R_, _C_: the sets of integers, rational numbers, real numbers, and complex numbers respectively.
• NULLSET: the empty set, i.e. the set with no elements
• _Set_: the proper class of all sets.
• _ADD_DEF_: the proper class of all mathematical objects such that the addition operation is defined, with respect to some domain.
• _MULT_DEF_: the proper class of all mathematical objects such that the multiplication operation is defined, with respect to some domain.
• _ADD_DEF_: the proper class of all mathematical objects such that both the addition and the multiplication operations are defined, with respect to some domain.

• NOT ___
• This keyword applies the operation of logical negation to its single argument. It is applied immediately, before any attempt to reason about the statement below it is made. If the argument is not interpretable as true or false, Franci considers the statement to have a syntax error. Note:
• NOT NOT cancels: Franci ignores it.
• NOT UNKNOWN := UNKNOWN
• NOT CONTRADICTION := CONTRADICTION
• NOT TRUE := FALSE
• NOT FALSE := TRUE

• ___^-1
• This keyword currently applies multiplicative inverse to its argument. It does not trigger type inference, since there are other legitimate interpretations.

• AND, OR, IFF, XOR, NXOR, NIFF, NOR, NAND, IMPLIES, NIMPLIES
• All of these keywords check to see that their arguments are interpretable as true or false. If either argument is not interpretable as true or false, this is a syntax error.
• AND, OR, IFF, and IMPLIES are interpreted in their usual mathematical usage when applied to TRUE and FALSE.
• XOR is interpreted as 'exclusive or'.
• A NXOR B := NOT (A XOR B)
• A NIFF B := NOT (A IFF B)
• A NOR B := NOT (A OR B)
• A NAND B := NOT (A AND B)
• A NIMPLIES B := NOT (A IMPLIES B)
• As of version 0.3.8.9, Franci correctly handles generalized associativity for 2-ary keywords.
• E.g., Franci considers X AND Y AND Z unambiguous.
• The keywords AND, OR have generalized associativity.
• As of version 0.3.9.2, Franci correctly handles transitivity for 2-ary keywords.
• E.g., Franci understands the difference between X IFF Y IFF Z and X IFF (Y IFF Z)
• The keyword IFF is transitive.
• +
• This is the addition operation. Franci also understands - as both infix subtraction, and as specifying additive inverse. Examples of legitimate addition (and subtraction) phrases:
• 1+1 evaluates to 2.
• X-X evaluates to 0. X does not have to be declared in advance.
• -123 means exactly what it looks like. Franci considers this to be an integer.
• X+26-47 evaluates to X-21. If X has not already been declared, Franci improvises it as an element of the class _ADD_DEF_.
• -X is simply the additive inverse of X.
• ·
• This is the multiplication operation. Examples of legitimate multiplication phrases:
• 1·X evaluates to X. If X is not defined, X is improvised to type _ADD_DEF_ because this is the most general context in which an element can be multiplied by an integer.
• 2·4^-1 evaluates to 2^-1
• Franci accepts the following HTML representations for · : ·, ^., and ·.

• AND, OR, IFF, XOR, NXOR, NIFF, NOR, NAND
• All of these keywords check to see that their arguments are interpretable as true or false. If any argument is not interpretable as true or false, this is a syntax error.
• the interpretation commentary for prefix n-ary keywords is the same as their infix 2-ary forms. They require at least two arguments, and are practically limited only by RAM.
• NXOR(A,B,C) := NOT XOR(A,B,C)
• NIFF(A,B,C) := NOT IFF(A,B,C)
• NOR(A,B,C) := NOT OR(A,B,C)
• NAND(A,B,C) := NOT AND(A,B,C)
• ALLEQUAL, ALLDISTINCT, NOTALLDISTINCT, NOTALLEQUAL
  • ALLEQUAL(A,B,C) indicates that any pair of the n[=3] arguments is semantically equal.
  • ALLDISTINCT(A,B,C) indicates that any pair of the n[=3] arguments is semantically distinct.
  • NOTALLDISTINCT(A,B,C) := NOT ALLDISTINCT(A,B,C)
  • NOTALLEQUAL(A,B,C) := NOT ALLEQUAL(A,B,C)
  • However, for 2-ary versions:
    • NOTALLDISTINCT(A,B) immediately reduces to ALLEQUAL(A,B)
    • NOTALLEQUAL(A,B) immediately reduces to ALLDISTINCT(A,B)
    • ALLEQUAL(A,B) := NOT ALLDISTINCT(A,B)
• EQUALTOONEOF, DISTINCTFROMALLOF
• These keywords do almost no syntax checking (beyond that their arguments are syntactically correct). I advise that non-free variables be explicitly declared in advance.
• These clauses, when used as arguments to other clauses, should be enclosed in parentheses.
• A EQUALTOONEOF B,C indicates A is equal to at least one of B or C.
• A DISTINCTFROMALLOF B,C indicates A is distinct from all of B, C
• A EQUALTOONEOF B,C := NOT (A DISTINCTFROMALLOF B,C)
• However, for 2-ary versions:
• A EQUALTOONEOF B immediately reduces to ALLEQUAL(A,B)
• A DISTINCTFROMALLOF B immediately reduces to ALLDISTINCT(A,B)

• Franci, Math Consultant™
• Franci logfile™
• Franci script language™

Return to the main page.