Skip to content

Logic Expressions

Jump to bottom
Octav Popescu edited this page Jun 28, 2023 · 98 revisions

Logic Expressions

CTAT comes with a module that allows manipulation of propositional logic expressions. The module consists of a grammar and functions for parsing, generating, evaluating, searching, testing, comparing, and performing various transformations on logic expressions.

All functions that take expressions as arguments can work with either strings or parse trees generated in previous function calls. Authors should not rely on a particular structure of these parse trees, as that could change without notice in the future. All tree manipulation should be done through the functions below.

All functions that return expressions can generate them either as strings or parse trees. The result type is the same as the argument type, except for logicParse and logicStringify, which are meant to convert between the two types. When a function takes two or more expressions as arguments, the result type follows the type of the first expression.

Search functions (logicFindOperator, logicFindExpresion, logicFindRuleApplication) return parse tree results that contain location information. This information is useful to guide or improve efficiency of later replacement operations. Authors should not rely on the particular structure of this location information, as it could change without notice.

Some functions can take a few option parameters that affect how the function is working or what kind of results it is returning. These options are accepted as an optional javascript object where the keys are the parameter names and the values select the various options (most often true or false).

On demand through an option parameter, some functions can return extra information, like the number of steps applied in case of simplification functions. When such functions are used with parse trees, the extra information is attached as a property of the parse tree result. When they are used with strings, the resulting strings are boxed in a corresponding class object, so the property can be attached to it.

By default functions return null if they run into an error (like a parse error for instance). This behavior can be changed using the parseErrors parser option below. Occasionally a function might return undefined, such cases are documented explicitly below.

Logic Language

The logic expressions accepted by the logic grammar consist of a set of operands connected with operators specific to propositional logic. Parentheses can also be used to group subexpressions inside larger expressions (or even around the whole expression, although it won't have any effect in this case).

  • Operands can be either logic variables (representing propositions) or logic constants (true and false).
    • Logic variables are represented by single letters, either upper case or lower case, optionally followed by one or more digits.
    • Logic constants are represented by the symbols ⊤, TRUE, true, T, 1 for true, and ⊥, FALSE, false, F, 0 for false.
  • Operators are any of the following list, in precedence order (with the associated accepted representations):
    • NOT: negation, unary operator represented by one of: ¬, ~, !, -
    • AND: conjunction, binary operator represented by one of: ∧, /\, &, &&, *, .
    • NAND: negated conjunction, binary operator represented by one of: ⊼, ↑, ~/\, ~&, ~&&, !/\, !&, !&&, -/\, -&, -&&
    • OR: disjunction, binary operator represented by one of: ∨, \/, |, ||, +
    • NOR: negated disjunction, binary operator represented by one of: ⊽, ↓, ~\/, ~|, ~||, !\/, !|, !||, -\/, -|, -||
    • IF: implication, binary operator represented by one of: →, ⇒, ⊃, =>, ->
    • IFF: bi-implication, binary operator represented by one of: ↔, ⇔, ≡, ⊙, <=>, <->, =
    • XOR: exclusive disjunction, binary operator represented by one of: ⊕, ≠, ≢, ⊻, ^, <~>

For generated expressions, the grammar will use the first symbol in each group by default. This can be changed through the use of language options, see below.

Examples of propositional logic expressions

¬(¬P ∨ ¬Q)
¬P ∨ ¬R ∧ Q
P → Q → R ↔ P ∧ Q → R
¬((P ∨ Q) ∧ ¬R)

Language/parser options

The accepted language can be customized through a number of options set with the help of the logicSetOptions function. These options are:

  • strictParentheses: In strict parentheses mode all binary operator subexpressions need to be enclosed in parentheses when used as operands in other expressions. In non-strict parentheses mode there's no such requirement, the parser using usual rules of precedence and associativity to interpret the expression. The default is false.

    Examples of strict parentheses mode expressions

    ¬P ∨ (¬R ∧ Q)
(P ∨ R) ∨ Q

    Examples of non-strict parentheses mode expressions

    ¬P ∨ ¬R ∧ Q
P ∨ R ∨ Q

  • operatorSymbols: This option specifies the symbols the grammar will use for the given operators in generated expressions, and also the operator symbols it will accept when parsing expressions with strictOperators mode enabled. The defaults are all symbols listed above for parsing, and the first symbols in each list for generation.

  • strictOperators: In strict operators mode the grammar will only accept operators represented as one of the symbols in the list given as the operatorSymbols option. In non-strict operators mode the grammar will accept all operator symbols listed above. The default is false.

  • constantSymbols: This option specifies the symbols the grammar will use for constants (true, false) in generated expressions, and also the constant symbols it will accept when parsing expressions with strictOperators mode enabled. The defaults are all symbols listed above for parsing, and the first symbols in each list for generation.

  • strictConstants: In strict constants mode the grammar will only accept constants represented as one of the symbols in the list given as the constantSymbols option. In non-strict constants mode the grammar will accept all constant symbols listed above. The default is false.

  • parseErrors: When set to true, it lets functions raise an exception on errors like ungrammatical expressions. When false, in case of an error these functions return null.

Transformation Rules

Some of the functions below take one or a list of transformation rules, and they apply those rules to expressions given as arguments. These rules correspond to propositional logic axioms or theorems. Most rules can be applied in two different directions, as indicated below. The forward direction is taken to be the direction that is useful in the process of reducing an expression to one of the normal forms, even if it results in a more complex expression. Here's a list of the rules that can be applied to expressions. The transformation formulas below are considered formula schemas, in that the variables can be consistently substituted with any other expressions.

Index

truthValues

  • Description: Transforms negated logic constants into the opposite values.
  • Formulas:
    • forward:
      ¬TRUE => FALSE
      ¬FALSE => TRUE
    • reverse:
      TRUE => ¬FALSE
      FALSE => ¬TRUE

domination

  • Description: Reduces conjunction/disjunction expressions to constants. Can only be applied in forward direction.
  • Formulas:
    • forward:
      P ∧ FALSE => FALSE
      P ∨ TRUE => TRUE
    • reverse: N/A

negation

  • Description: Reduces conjunction/disjunction expressions with opposite terms to constants. Can only be applied in forward direction.
  • Formulas:
    • forward:
      P ∧ ¬P => FALSE
      P ∨ ¬P => TRUE
    • reverse: N/A

identity

  • Description: Removes or adds redundant constants from conjunction/disjunction expressions.
  • Formulas:
    • forward:
      P ∧ TRUE => P
      P ∨ FALSE => P
    • reverse:
      P => P ∧ TRUE
      P => P ∨ FALSE

idempotence

  • Description: Removes redundant terms from conjunction/disjunction expressions.
  • Formulas:
    • forward:
      P ∧ P => P
      P ∨ P => P
    • reverse:
      P => P ∧ P
      P => P ∨ P

absorption

  • Description: Removes redundant terms from staggered conjunction/disjunction expressions. Can only be applied in forward direction.
  • Formulas:
    • forward:
      P ∧ (P ∨ Q) => P
      P ∨ (P ∧ Q) => P
    • reverse: N/A

inverseAbsorption

  • Description: Removes redundant inverse terms from staggered conjunction/disjunction expressions. Can only be applied in forward direction.
  • Formulas:
    • forward:
      P ∧ (¬P ∨ Q) => P ∧ Q
      P ∨ (¬P ∧ Q) => P ∨ Q
    • reverse: N/A

commutativity

  • Description: Reversed order of operands for conjunction/disjunction expressions. The two directions have identical effect.
  • Formulas:
    • forward:
    • reverse:
      P ∧ Q => Q ∧ P
      P ∨ Q => Q ∨ P

associativity

  • Description: Flattens staggered conjunction/disjunction expressions with the same operator. The two directions have identical effect.
  • Formulas:
    • forward:
    • reverse:
      P ∧ (Q ∧ R) => P ∧ Q ∧ R
      P ∨ (Q ∨ R) => P ∨ Q ∨ R

distributivity

  • Description: Spreads one operator over the other in staggered conjunction/disjunction expressions.
  • Formulas:
    • forward:
      P ∧ (Q ∨ R) => (P ∧ Q) ∨ (P ∧ R)
      P ∨ (Q ∧ R) => (P ∨ Q) ∧ (P ∨ R)
    • reverse:
      (P ∧ Q) ∨ (P ∧ R) => P ∧ (Q ∨ R)
      (P ∨ Q) ∧ (P ∨ R) => P ∨ (Q ∧ R)

deMorgan

  • Description: Spreads negation over terms of conjunction/disjunction expressions.
  • Formulas:
    • forward:
      ¬(P ∧ Q) => ¬P ∨ ¬Q
      ¬(P ∨ Q) => ¬P ∧ ¬Q
    • reverse:
      ¬P ∨ ¬Q => ¬(P ∧ Q)
      ¬P ∧ ¬Q => ¬(P ∨ Q)

doubleNegation

  • Description: Eliminates two successive negation operators.
  • Formulas:
    • forward:
      ¬¬P => P
    • reverse:
      P => ¬¬P

implication

  • Description: Eliminates or introduces an implication operator based on its definition.
  • Formulas:
    • forward:
      P → Q => ¬P ∨ Q
    • reverse:
      ¬P ∨ Q => P → Q

biimplication

  • Description: Eliminates or introduces an bi-implication operator based on its definition.
  • Formulas:
    • forward:
      P ↔ Q => (P ∧ Q) ∨ (¬P ∧ ¬Q)
    • reverse:
      (P ∧ Q) ∨ (¬P ∧ ¬Q) => P ↔ Q

biimplicationToImplication

  • Description: Eliminates or introduces an bi-implication operator based on a definition involving implication operators.
  • Formulas:
    • forward:
      P ↔ Q => (P → Q) ∧ (Q → P)
    • reverse:
      (P → Q) ∧ (Q → P) => P ↔ Q

exclusiveDisjunction

  • Description: Eliminates or introduces an exclusive disjunction operator based on its definition.
  • Formulas:
    • forward:
      P ⊕ Q => (¬P ∧ Q) ∨ (P ∧ ¬Q)
    • reverse:
      (¬P ∧ Q) ∨ (P ∧ ¬Q) => P ⊕ Q

exclusiveDisjunctionToImplication

  • Description: Eliminates or introduces an exclusive disjunction operator based on a definition involving implication operators.
  • Formulas:
    • forward:
      P ⊕ Q => (P → ¬Q) ∧ (¬Q → P)
    • reverse:
      (P → ¬Q) ∧ (¬Q → P) => P ⊕ Q

Function Index

Basic Functions

These functions perform basic operations on expressions, like parsing, generating strings, sorting, evaluating, etc.

logicSetOptions

logicSetOptions(object = {})

  • Arguments:
    • object - an option object containing settings as key-value pairs
  • Result: the object argument
  • Description: Sets the language/parser options to the settings given in the input object. These options are described in section Language/parser options above. Several options can be set in the same object. Returns the current set of options.
  • Usage Examples:
    logicSetOptions({strictParentheses: true}) sets the language to strict parentheses mode
    logicSetOptions({operatorSymbols: {NOT: '~', AND: '&', OR: '|'}) sets the language operator symbols to the ones specified in the given object
    logicSetOptions({strictOperators: true}) sets the language to strict operators mode
    logicSetOptions({constantSymbols: {true: 'TRUE', false: 'FALSE'}) sets the language constant symbols to the ones specified in the given object
    logicSetOptions({strictConstants: true}) sets the language to strict constant mode
    logicSetOptions({parseErrors: true}) sets the parser to the mode where it will raise exceptions in case of errors

logicParse

logicParse(expression)

  • Arguments:
    • expression - a logic expression to parse, as a string or a tree
  • Result: a parse tree representing the given expression
  • Description: Parses the given expression and returns the parse tree. If the expression cannot be parsed, it returns null or raises a parse error, depending on the value of the parseErrors option. If the expression is already a parse tree it is returned unchanged.
  • Usage Examples:
    logicParse('¬P ∨ ¬R ∧ Q') => a parse tree representing the expression

logicGetError

logicGetError(expression)

  • Arguments:
    • expression - a logic expression to parse, as a string or a tree
  • Result: an error object describing a parse error generated while parsing the given expression
  • Description: Parses the given expression and returns null if successful. If the expression cannot be parsed, it returns the error object generated during the parse. The error object contains two properties: a message string and a hash of additional information. If the expression is already a parse tree it also returns null.
  • Usage Examples:
    logicGetError('¬P ∨ ¬R ∧ Q') => an error in strictParentheses mode

logicStringify

logicStringify(expression)

  • Arguments:
    • expression - a logic expression to stringify, as a string or a tree
  • Result: a logic expression string representing the given expression
  • Description: Generates a logic expression string representing the same expression as the input parse tree. When strictParentheses language option is false, the generated expression will only have the minimum number of parentheses necessary to keep the original expression structure. If strictParentheses is true, each binary operator will have its subexpression enclosed in parentheses. If the input expression is a string it is returned unchanged.
  • Usage Examples:
    logicStringify(t) => ¬P ∨ ¬R ∧ Q if t is the tree generated from the same expression by logicParse
    logicStringify(t) => ¬P ∨ (¬R ∧ Q) for the same tree with strictParentheses set to true

logicEvaluate

logicEvaluate(expression, bindings = null)

  • Arguments:
    • expression - a logic expression to evaluate, as a string or a tree
    • bindings - an optional object representing an object of variable bindings
  • Result: a logic value (true or false) representing the expression value, or undefined if unknown
  • Description: Returns a logic value determined by evaluating the given logic expression according to the operators' truth tables. Variables in the expression are evaluated against their values in the bindings object, if present, otherwise in the tutor's variable table. The bindings object should be either a generic object whose properties are the variable names, or an object that implements a get method, taking a variable name as an argument. Missing variables are considered unknown, which might lead to the whole expression to evaluate to unknown. In this case the function returns undefined.
  • Usage Examples:
    logicEvaluate('P ∧ TRUE', {P: 'FALSE'}) => false
    logicEvaluate('P ∧ TRUE', {P: 'TRUE'}) => true
    logicEvaluate('P ∧ TRUE') => undefined
    logicEvaluate('P ∨ TRUE') => true no matter what the value of variable P is

logicSort

logicSort(expression)

  • Arguments:
    • expression - a logic expression to sort, as a string or a tree
  • Result: a logic expression as a string or a tree, representing the sorted expression
  • Description: Returns the expression sorted structurally. The sorting moves more complex subexpressions towards the end of the expression.
  • Usage Examples:
    logicSort('¬R ∧ Q ∨ ¬P') => '¬P ∨ Q ∧ ¬R'

Expression Inspection

These functions search a given expression for generic types of elements and return the elements found.

logicGetMainOperator

logicGetMainOperator(expression, {symbol = false})

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
    • symbol - an option boolean indicating whether the result should be the actual symbol used, or rather the operator name
  • Result: an operator string representing the main operator in the expression
  • Description: Returns the main operator of the given expression. If symbol is true, it will return the actual symbol used in the expression, otherwise it will return the operator name in the operator list above.
  • Usage Examples:
    logicGetOperator('¬R ∧ Q ∨ ¬P') => 'OR'
    logicGetOperator('¬(¬P ∨ ¬Q)', {symbol: true}) => '¬'
    logicGetOperator('P → Q → R ↔ P ∧ Q → R') => 'IFF'

logicGetOperators

logicGetOperators(expression, {symbols = false})

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
    • symbols - an option boolean indicating whether the results should be the actual symbols used, or rather operator names
  • Result: an array of operator strings representing all operators in the expression
  • Description: Returns the list (as a Javascript array) of operators in the given expression. If symbols is true, it will return the actual symbols used in the expression, otherwise it will return the operator names in the operator list above. The list is sorted by the order of the operators in the expression (inorder tree traversal) and can contain duplicates.
  • Usage Examples:
    logicGetOperators('¬R ∧ Q ∨ ¬P') => ['NOT', 'AND', 'OR', 'NOT']
    logicGetOperators('¬(¬P ∨ ¬Q)', {symbols: true}) => ['¬', '¬', '∨', '¬']
    logicGetOperators('P → Q → R ↔ P ∧ Q → R') => ['IF', 'IF', 'IFF', 'AND', 'IF']

logicGetVariables

logicGetVariables(expression)

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
  • Result: an array of strings representing all variables in the expression
  • Description: Returns the list (as a Javascript array) of variables names in the given expression. The list is sorted by the order of the variables in the expression (inorder tree traversal) and can contain duplicates.
  • Usage Examples:
    logicGetVariables('¬R ∧ Q ∨ ¬P') => ['R', 'Q', 'P']
    logicGetVariables('¬(¬P ∨ ¬Q)') => ['P', 'Q']
    logicGetVariables('P → Q → R ↔ P ∧ Q → R') => ['P', 'Q', 'P', 'Q', 'R']

logicGetOperands

logicGetOperands(expression)

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
  • Result: an array of subexpressions as strings or trees, representing the operands for the main expression operator
  • Description: Returns the list (as a Javascript array) of operands for the main operator in the given expression. The components of the list are either strings or parse trees, depending on the type of the given expression. The list is sorted in the order the operands occur in the expression.
  • Usage Examples:
    logicGetOperands('¬R ∧ Q ∨ ¬P') => ['¬R ∧ Q', '¬P']
    logicGetOperands('¬(¬P ∨ ¬Q)') => ['¬P ∨ ¬Q']
    logicGetOperands('P → Q → R ↔ P ∧ Q → R') => ['P → Q → R', 'P ∧ Q → R']

logicGetExpression

logicGetExpression(expression, {start = 0, end = last + 1})

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
    • start - an option integer representing the start operand index (defaulting to 0)
    • end - an option integer representing the index past the end operand (defaulting to the end of the expression)
  • Result: a subexpression as string or tree, representing the given expression's main operator with a selected range of operands
  • Description: Returns a subexpression with the same operator as the main operator in the given expression, and the operands a subrange of the operands of the given expression's main operator, between indices start and end - 1. If the range includes only 1 operand (start + 1 = end), the respective operand is returned as is. If start < 0 or end > last + 1, 0 or last + 1 are used instead. If start ≥ end the result is undefined. Operands can be subexpressions.
  • Usage Examples:
    logicGetExpression('¬R ∧ Q ∧ ¬P', {start: 0, end: 2}) => '¬R ∧ Q'
    logicGetExpression('¬P ∨ ¬Q ∨ R ∧ S', {start: 1}) => '¬Q ∨ R ∧ S'
    logicGetExpression('¬P ∧ Q ∨ ¬Q ∧ R') => '¬P ∧ Q ∨ ¬Q ∧ R'
    logicGetExpression('¬P ∧ Q ∨ ¬Q ∧ R', {start: 1, end: 2}) => '¬Q ∧ R'

Expression Search

These functions search a given expression for occurrences of specific elements and return a list of subexpressions that contains those elements. Depending on an option, the result might contain location information that can be used in subsequent transformation operations.

logicFindOperator

logicFindOperator(expression, operator, {paths = false})

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
    • operator - an operator string representing the name of the operator to search for
    • paths - an option boolean indicating whether to return location information in the result
  • Result: an array of expressions as (possibly boxed) strings or trees, representing subexpressions with the given operator
  • Description: Returns a list of subexpressions of the given expression (including possibly the whole expression) that have the given operator as its main operator. The operator is one of the string names in the list of operators above. The list is sorted by the order of the subexpression operators in the expression (inorder tree traversal).
    If paths is set to true, the result will include location information in the form of paths that can be used subsequently in transformation operations. If the results are strings, they will be boxed in objects of String type, so path information can be attached.
  • Usage Examples:
    logicFindOperator('¬(¬P ∨ ¬Q)', 'NOT') => ['¬(¬P ∨ ¬Q)', '¬P', '¬Q']
    logicFindOperator('P → Q → R ↔ P ∧ Q → R', 'IF') => ['P → Q → R', 'Q → R', 'P ∧ Q → R']
    logicFindOperator('P ∧ Q ∧ R', 'AND') => ['P ∧ Q', 'P ∧ Q ∧ R']
    logicFindOperator('P ∧ Q ∧ R', 'AND', {paths: true}) => [[String: 'P ∧ Q'] {path: [[0, 2]]}, [String: 'P ∧ Q ∧ R'] {path: []}]

logicFindExpression

logicFindExpression(expression, subexpression, {paths = false}))

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
    • subexpression - a logic subexpression to search for, as a string or a tree
    • paths - an option boolean indicating whether to return location information in the result
  • Result: an array of expressions as strings or trees, representing subexpressions equal to the given subexpression
  • Description: Returns a list of subexpressions of the given expression (including possibly the whole expression) that are equal to the given subexpression. The test is done at the parse tree level, not at the string level. The list is sorted by the order of the subexpression operators in the expression (inorder tree traversal). If paths is set to true, the result will include location information in the form of paths that can be used subsequently in transformation operations. If the results are strings, they will be boxed in objects of String type, so path information can be attached.
  • Usage Examples:
    logicFindExpression('P → Q → R ↔ P ∧ Q → R', 'Q → R') => ['Q → R']
    logicFindExpression('P ∨ Q ∨ R ∨ S', 'Q ∨ R', {paths: true}) => [String: 'Q ∨ R'] {path: [[1, 3]]}

logicFindRuleApplication

logicFindRuleApplication(expression, rule, {reverse = false, paths = false})

  • Arguments:
    • expression - a logic expression to search, as a string or a tree
    • rule - a rule name string to search for
    • reverse - an option boolean indicating application direction
    • paths - an option boolean indicating whether to return location information in the result
  • Result: an array of expressions as strings or trees, representing subexpressions that the given rule can be applied to in the indicated direction
  • Description: Returns a list of subexpressions of the given expression, where each subexpression is a possible target for applying the rule specified in the second argument. The rule name is one of the names in the list of rules in section Transformation Rules. reverse specifies whether the rule should be applied in 'reverse' direction, see the rule descriptions. The list is sorted in the order of the subexpression operators in the expression (inorder tree traversal). If paths is set to true, the result will include location information in the form of paths that can be used subsequently in transformation operations. If the results are strings, they will be boxed in objects of String type, so path information can be attached.
  • Usage Examples:
    logicFindRuleApplication('¬(¬P ∨ ¬Q)', 'deMorgan') => ['¬(¬P ∨ ¬Q)']
    logicFindRuleApplication('¬(¬P ∨ ¬Q)', 'deMorgan', {reverse: true}) => ['¬P ∨ ¬Q']
    logicFindRuleApplication('¬(¬P ∨ ¬Q)', 'deMorgan', {reverse: true, paths: true}) [[String: '¬P ∨ ¬Q'] {path: ['right']}]
    logicFindRuleApplication('P → Q → R ↔ P ∧ Q → R', 'implication') => ['P → Q → R', 'Q → R', 'P ∧ Q → R']

Expression Transformations

These functions perform specific transformations on given expressions.

logicApplyRules

logicApplyRules(expression, rules, {reverse = false, global = false})

  • Arguments:
    • expression - a logic expression to transform, as a string or a tree
    • rules - a rule name string or an array of rule name strings to apply
    • reverse - an option boolean indicating direction
    • global - an option boolean indicating transformation scope
  • Result: an expression as a string or tree, representing the result of applying the given rules to the given expression
  • Description: Returns an expression that is the result of applying the rule or rules in the given second argument to the expression in the first argument. reverse indicates whether the rules are applied in the 'reverse' direction. global indicates whether the rules are applied to the whole expression rather than only to the main operator in the expression.
  • Usage Examples:
    logicApplyRules('¬(¬P ∨ ¬Q)', 'deMorgan') => '¬¬P ∧ ¬¬Q'
    logicApplyRules('¬(¬P ∨ ¬Q)', 'deMorgan', {reverse: true, global: true}) => '¬¬(P ∧ Q)'
    logicApplyRules('P → Q → R ↔ P ∧ Q → R', 'implication', {global: true}) => '¬P ∨ (¬Q ∨ R) ↔ ¬(P ∧ Q) ∨ R'

logicCreateExpression

logicCreateExpression(operator, expressions...)

  • Arguments:
    • operator - an operator string to use in new expression
    • expressions... - a sequence of one or more logic expressions, each specified as a string or a tree
  • Result: a new expression as a string or tree, representing the result of creating a new expression with the given operator and operands
  • Description: Returns a new expression created by using the given operator as the main operator and the given expressions... as its operands. Returns null if not enough operands are provided. Ignores any extra operands (but 'AND' and 'OR' operators can take any number of operands higher or equal than 2). The operator is one of the string names in the list of operators above.
  • Usage Examples:
    logicCreateExpression('OR', 'P', 'Q ∨ P ∧ S') => 'P ∨ (Q ∨ P ∧ S)'
    logicCreateExpression('AND', 'P ∨ Q ∨ P ∧ S', 'Q') => '(P ∨ Q ∨ P ∧ S) ∧ Q'

logicReplaceExpression

logicReplaceExpression(expression, oldsubexpression, newsubexpression, {index = 0})

  • Arguments:
    • expression - a logic expression to change, as a string or a tree
    • oldsubexpression - a logic subexpression to replace, as a string or a tree
    • newsubexpression - a logic subexpression to replace with, as a string or a tree
    • index - an option integer representing the old subexpression index
  • Result: an expression as a string or tree, representing the result of the replacement
  • Description: Returns a new expression that is the result of replacing the oldsubexpression with the newsubexpression in the given expression. The index parameter can be a 0-based index used to select among multiple occurrences of the given oldsubexpression. If the index parameter is missing and oldsubexpression is obtained through a previous logicFind... call with a paths option of true, it already contains location information allowing for its efficient retrieval within expression. If subexpression does not include location information, index defaults to 0.
  • Usage Examples:
    logicReplaceExpression('P ∨ Q ∨ P ∧ S', 'P', 'V ∧ W', {index: 0}) => 'V ∧ W ∨ Q ∨ P ∧ S'
    logicReplaceExpression('P ∨ Q ∨ P ∧ S', 'P', 'V ∧ W', {index: 1}) => 'P ∨ Q ∨ (V ∧ W) ∧ S'

logicDeleteExpression

logicDeleteExpression(expression, subexpression, {index = 0})

  • Arguments:
    • expression - a logic expression to change, as a string or a tree
    • subexpression - a logic subexpression to delete, as a string or a tree
    • index - an option integer representing the subexpression index
  • Result: an expression as a string or tree, representing the result of the deletion
  • Description: Returns a new expression that is the result of deleting the subexpression, together with its corresponding operators, from the given expression. The index parameter can be a 0-based index used to select among multiple occurrences of the given subexpression. If the index parameter is missing and subexpression is a parse tree obtained through a previous logicFind... call with a paths option of true, it already contains location information allowing for its efficient retrieval within expression. If subexpression does not include location information, index defaults to 0.
  • Usage Examples:
    logicDeleteExpression('P ∨ Q ∨ P ∧ S', 'P', {index: 0}) => 'Q ∨ P ∧ S'
    logicDeleteExpression('P ∨ Q ∨ P ∧ S', 'P', {index: 1}) => 'P ∨ Q ∨ S'

Expression Simplifications

These functions perform normalization of the given expressions to one of the three normal forms (negative, disjunctive, conjunctive) and also perform additional simplifications validated by propositional logic axioms with the aim of achieving the simplest normalized expressions. The resulting expressions are also ordered alphabetically.

logicSimplifyNNF

logicSimplifyNNF(expression, {steps = false})

  • Arguments:
    • expression - a logic expression to simplify as a string or a tree
    • steps - an option boolean indicating whether the result should include the number of steps
  • Result: a negative normal form expression equivalent to the given expression, as a string or tree
  • Description: Returns an expression that represents the given expression reduced to negative normal form and simplified. If steps is true, then the result will add a steps field that counts the number of steps in the simplification process.
  • Usage Examples:
    logicSimplifyNNF('¬(¬P ∨ ¬Q)') => 'P ∧ Q'
    logicSimplifyNNF('¬((P ∨ Q) ∧ ¬R)', {steps: true}) => [String: 'R ∨ ¬P ∧ ¬Q'] {steps: 5}

logicSimplifyCNF

logicSimplifyCNF(expression, {steps = false})

  • Arguments:
    • expression - a logic expression to simplify as a string or a tree
    • steps - an option boolean indicating whether the result should include the number of steps
  • Result: a conjunctive normal form expression equivalent to the given expression, as a string or tree
  • Description: Returns an expression that represents the given expression reduced to conjunctive normal form and simplified. If steps is true, then the result will add a steps field that counts the number of steps in the simplification process.
  • Usage Examples:
    logicSimplifyCNF('¬(¬P ∨ ¬Q)') => 'P ∧ Q'
    logicSimplifyCNF('¬((P ∨ Q) ∧ ¬R)', {steps: true}) => [String: '(¬P ∨ R) ∧ (¬Q ∨ R)'] {steps: 6}

logicSimplifyDNF

logicSimplifyDNF(expression, {steps = false})

  • Arguments:
    • expression - a logic expression to simplify as a string or a tree
    • steps - an option boolean indicating whether the result should include the number of steps
  • Result: a disjunctive normal form expression equivalent to the given expression, as a string or tree
  • Description: Returns an expression that represents the given expression reduced to disjunctive normal form and simplified. If steps is true, then the result will add a steps field that counts the number of steps in the simplification process.
  • Usage Examples:
    logicSimplifyDNF('¬(¬P ∨ ¬Q)') => 'P ∧ Q'
    logicSimplifyDNF('¬((P ∨ Q) ∧ ¬R)', {steps: true}) => [String: 'R ∨ ¬P ∧ ¬Q'] {steps: 15}

Basic Expression Tests

These functions perform basic tests corresponding to some of the functions in section Basic Functions, that is they test whether the given expression would return a valid result or the same result when one of the basic functions is called on it.

logicValid

logicValid(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indication whether the given expression is valid or not
  • Description: Returns a boolean value that indicates whether the given expression is valid or not. Expression validity is checked by attempting to parse it. It corresponds to function logicParse.
  • Usage Examples:
    logicValid('¬(¬P ∨ ¬Q)') => true
    logicValid('¬(¬P ∨ ¬Q') => false

logicValued

logicValued(expression, bindings = null)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
    • bindings - an optional object representing a list of variable bindings
  • Result: a boolean value indicating whether the given expression has a value or is unknown
  • Description: Returns a boolean value that indicates whether the given expression can be evaluated to a logic value or not (because some variables might be unknown). The test is performed by attempting to evaluate the expression using function logicEvaluate. Variables in the expression are evaluated against their values in the bindings object, if present, otherwise in the tutor's variable table. The bindings object should be either a generic object whose properties are the variable names, or an object that implements a get method, taking a variable name as an argument. Missing variables are considered unknown, in which case the function returns false. It corresponds to function logicEvaluate.
  • Usage Examples:
    logicValued('¬(¬P ∨ ¬Q)') => false
    logicValued('¬(¬P ∨ ¬Q)', {P: true, Q: false}) => true

logicSorted

logicSorted(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indicating whether the given expression is sorted
  • Description: Returns a boolean value that indicates whether the given expression is sorted. The testing is done by sorting the expression and comparing the result against the original parsed expression. It corresponds to function logicSort.
  • Usage Examples:
    logicSorted('¬((P ∨ Q) ∧ ¬R)') => false
    logicSorted('¬(¬R ∧ (P ∨ Q))') => true

Expression Normal Form Tests

These functions test whether the given expression satisfies the criteria for one of the three normal forms (negation, disjunction, conjunction). They don't correspond directly to the logicSimplify... functions in section Expression Simplifications, as they don't check if the expressions are also further simplified and sorted.

logicCheckNNF

logicCheckNNF(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indicating if the given expression is in NNF
  • Description: Returns a boolean value that indicates whether the given expression is in negative normal form. The test is done by checking the conditions for the negative normal form.
  • Usage Examples:
    logicCheckNNF('¬(¬P ∨ ¬Q)') => false
    logicCheckNNF('¬P ∨ ¬Q') => true

logicCheckCNF

logicCheckCNF(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indicating if the given expression is in CNF
  • Description: Returns a boolean value that indicates whether the given expression is in conjunctive normal form. The test is done by checking the conditions for the conjunctive normal form.
  • Usage Examples:
    logicCheckCNF('¬((P ∨ Q) ∧ ¬R)') => false
    logicCheckCNF('(P ∨ Q) ∧ ¬R') => true

logicCheckDNF

logicCheckDNF(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indicating if the given expression is in DNF
  • Description: Returns a boolean value that indicates whether the given expression is in disjunctive normal form. The test is done by checking the conditions for the disjunctive normal form.
  • Usage Examples:
    logicCheckDNF('(P ∨ Q) ∧ ¬R') => false
    logicCheckDNF('P ∧ ¬R ∨ Q ∧ ¬R') => true

Expression Simplification Tests

These functions test whether the given expression is simplified to one of the three normal forms (negation, disjunction, conjunction). They correspond to the logicSimplify... functions in section Expression Simplifications, tests being done by simplifying the expression to the corresponding normal form, and comparing the result against the original expression.

logicSimplifiedNNF

logicSimplifiedNNF(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indicating if the given expression is simplified NNF
  • Description: Returns a boolean value that indicates whether the given expression is in simplified negative normal form. The test is done by reducing the expression to negative normal form, simplifying it, and comparing the result against the original parsed expression. It corresponds to function logicSimplifyNNF.
  • Usage Examples:
    logicSimplifiedNNF('¬(¬P ∨ ¬Q)') => false
    logicSimplifiedNNF('¬P ∨ ¬Q') => true

logicSimplifiedCNF

logicSimplifiedCNF(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indicating if the given expression is simplified CNF
  • Description: Returns a boolean value that indicates whether the given expression is in simplified conjunctive normal form. The test is done by reducing the expression to conjunctive normal form, simplifying it, and comparing the result against the original parsed expression. It corresponds to function logicSimplifyCNF.
  • Usage Examples:
    logicSimplifiedCNF('¬((P ∨ Q) ∧ ¬R)') => false
    logicSimplifiedCNF('(P ∨ Q) ∧ ¬R') => true

logicSimplifiedDNF

logicSimplifiedDNF(expression)

  • Arguments:
    • expression - a logic expression to test as a string or a tree
  • Result: a boolean value indicating if the given expression is simplified DNF
  • Description: Returns a boolean value that indicates whether the given expression is in simplified disjunctive normal form. The test is done by reducing the expression to disjunctive normal form, simplifying it, and comparing the result against the original parsed expression. It corresponds to function logicSimplifyDNF.
  • Usage Examples:
    logicSimplifiedDNF('(P ∨ Q) ∧ ¬R') => false
    logicSimplifiedDNF('P ∧ ¬R ∨ Q ∧ ¬R') => true

Expression Comparison Tests

These functions perform comparison tests on two given expressions to determine if they are 'equivalent' from a specific point of view. They mostly work by applying one of the previous functions on the two expressions and comparing the results.

logicIdentical

logicIdentical(expression1, expression2)

  • Arguments:
    • expression1 - a logic expression to compare as a string or a tree
    • expression2 - a logic expression to compare as a string or a tree
  • Result: a boolean value indicating whether the given expressions are identical
  • Description: Returns a boolean value that indicates whether the two given expressions are identical. Identity is tested by parsing and sorting the two expressions and comparing the results, so two expressions ordered differently are still considered identical. It uses the function logicSort.
  • Usage Examples:
    logicIdentical('(P ∨ Q) ∧ ¬R', '¬R ∧ (P ∨ Q)') => true
    logicIdentical('(P ∨ Q) ∧ ¬R', 'P ∨ Q ∧ ¬R') => false

logicEqual

logicEqual(expression1, expression2, bindings = null)

  • Arguments:
    • expression1 - a logic expression to compare as a string or a tree
    • expression2 - a logic expression to compare as a string or a tree
    • bindings - an optional object representing a list of variable bindings
  • Result: a boolean value indicating whether the given expressions have the same value
  • Description: Returns a boolean value that indicates whether the two given expressions evaluate to the same logic value. The test is performed by evaluating the two expressions using function logicEvaluate, and comparing the results. Variables in the expression are evaluated against their values in the bindings object, if present, otherwise in the tutor's variable table. The bindings object should be either a generic object whose properties are the variable names, or an object that implements a get method, taking a variable name as an argument. If one of the two expressions evaluates to undefined, the comparison result is also undefined.
  • Usage Examples:
    logicEqual('P', 'Q', {P: true, Q: true}) => true
    logicEqual('P', 'Q', {P: true, Q: false}) => false
    logicEqual('P', 'Q') => undefined

logicEquivalent

logicEquivalent(expression1, expression2)

  • Arguments:
    • expression1 - a logic expression to compare as a string or a tree
    • expression2 - a logic expression to compare as a string or a tree
  • Result: a boolean value indicating whether the given expressions are equivalent
  • Description: Returns a boolean value that indicates whether the two given expressions are equivalent. The test is performed by reducing the two expressions to one of the simplified normal forms and comparing the results. It uses functions logicSimplifyCNF and logicSimplifyDNF.
  • Usage Examples:
    logicEquivalent('(P ∨ Q) ∧ ¬R', 'P ∧ ¬R ∨ Q ∧ ¬R') => true
    logicEquivalent('¬(¬P ∨ ¬Q)', 'P ∨ Q') => false

logicAlwaysEqual

logicAlwaysEqual(expression1, expression2, {counterexample = false})

  • Arguments:
    • expression1 - a logic expression to compare as a string or a tree
    • expression2 - a logic expression to compare as a string or a tree
    • counterexample - an option boolean indicating whether the result should include a counterexample
  • Result: a boolean value indicating whether the given expressions have always the same values (are semantically equivalent)
  • Description: Returns a boolean value that indicates whether the two given expressions are semantically equivalent. The test is performed by checking whether their values are the same for all combinations of truth values assigned to their variables. If counterexample is true and the expressions are not always equal, the result will be a boxed Boolean with an attached counterexample field that lists one set of variable bindings under which the expressions have different truth values.
  • Usage Examples:
    logicAlwaysEqual('(P ∨ Q) ∧ ¬R', 'P ∧ ¬R ∨ Q ∧ ¬R') => true
    logicAlwaysEqual('¬(¬P ∨ ¬Q)', 'P ∨ Q') => [Boolean false] {counterexample: {P: true, Q: false}}

logicFindCounterexampleValues

logicFindCounterexampleValues(expression1, expression2)

  • Arguments:
    • expression1 - a logic expression to compare as a string or a tree
    • expression2 - a logic expression to compare as a string or a tree
  • Result: a variable truth value binding set showing a case where the values of the given expressions are different
  • Description: Returns an object containing a list of variable bindings for which the two expressions have different values. The test is performed by checking whether their values are the same for all combinations of truth values assigned to their variables, and stopping when one is found where the values are different. If no difference is found for any truth values set, it returns undefined.
  • Usage Examples:
    logicFindCounterexampleValues('(P ∨ Q) ∧ ¬R', 'P ∧ ¬R ∨ Q ∧ ¬R') => undefined
    logicFindCounterexampleValues('¬(¬P ∨ ¬Q)', 'P ∨ Q') => {P: true, Q: false}

CTAT: Cognitive Tutor Authoring Tools, Software for authoring intelligent tutor behavior

CTAT Documentation

Getting Started
Using CTAT
HTML Components
TutorShop
Additional Documentation
In Development
Clone this wiki locally