Franci, Math Consultant™ : Description
Franci, Math Consultant™ is a mathematics AI program. I have been coordinating her
development during and after 1997. In this set of web pages, I will refer to Franci, Math
Consultant™ as Franci.
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's interactive user interface is most definitely pre-alpha. Her logfiles are much more
reliable -- for stable versions, a Franci logfile™ is mathematically correct.
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
Comments
- If a script line starts (after whitespace) with // , then Franci interprets this as a C++ comment.
She ignores the entire script line, silently.
Reserved commands
- 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 ___"
Reserved characters
- ( ) [ ] { } , ;
- ASCII space, or the start of the script line
0-ary keywords
- 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.
Prefix 1-ary keywords
- 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
Postfix 1-ary keywords
- ___-1
- This keyword currently applies multiplicative inverse to its argument. It does not
trigger type inference, since there are other legitimate interpretations.
-
Infix 2-ary keywords
- 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 · : ·, <sup>.</sup>, and ·.
Prefix n-ary keywords [only limits to the number of arguments (arity) are system RAM and human psychology. Examples are given for arity 3.]
- 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)
The following are trademarks owned by Kenneth Boyd:
- Franci, Math Consultant™
- Franci logfile™
- Franci script language™
Opinions, comments, criticism, etc.? Let me know about it.
Return to the main page.