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

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: ¬, ~, !, -
  • NAND: negated conjunction, binary operator represented by one of: ⊼, ↑, ~/\, ~&, ~&&, !/\, !&, !&&, -/\, -&, -&&
  • AND: conjunction, binary operator represented by one of: ∧, /\, &, &&, *, .
  • NOR: negated disjunction, binary operator represented by one of: ⊽, ↓, ~\/, ~|, ~||, !\/, !|, !||, -\/, -|, -||
  • OR: disjunction, binary operator represented by one of: ∨, \/, |, ||, +
  • NIF: negated implication, binary operator represented by one of: ↛, ⇏, ⊅, ≠>, ~>
  • IF: implication, binary operator represented by one of: →, ⇒, ⊃, =>, ->
  • XOR: exclusive disjunction, binary operator represented by one of: ⊕, ≠, ≢, ⊻, ^, <~>
  • IFF: bi-implication, 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.

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

The grammar applies the following precedence and associativity to the accepted operators, where lower numbers mean greater precedence.

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.

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.

• truthValues
• domination
• negation
• identity
• idempotence
• absorption
• inverseAbsorption
• commutativity
• associativity
• distributivity
• deMorgan
• doubleNegation
• negativeConjunction
• negativeDisjunction
• implication
• negativeImplication
• negativeImplicationToImplication
• biimplication
• biimplicationToImplication
• exclusiveDisjunction
• exclusiveDisjunctionToImplication

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

• 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

• 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

• 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

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

• 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

• 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

• 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

• 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

• 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)

• 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)

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

• Description: Eliminates or introduces a negative conjunction operator based on its definition.
• Formulas:
  • forward:
    P ⊼ Q => ¬(P ∧ Q)
  • reverse:
    ¬(P ∧ Q) => P ⊼ Q

• Description: Eliminates or introduces a negative disjunction operator based on its definition.
• Formulas:
  • forward:
    P ⊽ Q => ¬(P ∨ Q)
  • reverse:
    ¬(P ∨ Q) => P ⊽ Q

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

• Description: Eliminates or introduces a negative implication operator based on its definition.
• Formulas:
  • forward:
    P ↛ Q => P ∧ ¬Q
  • reverse:
    P ∧ ¬Q => P ↛ Q

• Description: Eliminates or introduces a negative implication operator based on a definition involving implication operators.
• Formulas:
  • forward:
    P ↛ Q => ¬(P → Q)
  • reverse:
    ¬(P → Q) => P ↛ Q

• 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

• 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

• 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

• 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 logicCheckTests below can take a list of tests to apply to a given expression. The section lists the tests currently implemented. The last four tests are used in specific normal form tests.

• atomic
• constant
• negationOperator
• conjunctionOperator
• disjunctionOperator
• negativeConjunctionOperator
• negativeDisjunctionOperator
• junctionOperator
• negativeJunctionOperator
• implicationOperator
• negativeImplicationOperator
• biimplicationOperator
• exclusiveDisjunctionOperator
• binaryOperator
• normalFormOperators
• atomicNegation
• atomicConjunction
• atomicDisjunction

• Description: Checks whether the expression is atomic, that is a variable or constant, negated or not.

• Description: Checks whether the expression is a constant.

• Description: Checks whether the expression's main operator is 'NOT'.

• Description: Checks whether the expression's main operator is 'AND'.

• Description: Checks whether the expression's main operator is 'OR'.

• Description: Checks whether the expression's main operator is 'NAND'.

• Description: Checks whether the expression's main operator is 'NOR'.

• Description: Checks whether the expression's main operator is 'AND' or 'OR'.

• Description: Checks whether the expression's main operator is 'NAND' or 'NOR'.

• Description: Checks whether the expression's main operator is 'IF'.

• Description: Checks whether the expression's main operator is 'NIF'.

• Description: Checks whether the expression's main operator is 'IFF'.

• Description: Checks whether the expression's main operator is 'XOR'.

• Description: Checks whether the expression's main operator is any except 'NOT'.

• Description: Checks whether all operators in the expression are 'NOT', 'AND', or 'OR'.

• Description: Verifies whether all negations are at the atomic level, as it would result from repeated application of the deMorgan transformation rule.

• Description: Verifies whether all conjunctions are at the atomic level, as it would result from repeated application of the distributivity transformation rule of conjunction over disjunction.

• Description: Verifies whether all disjunctions are at the atomic level, as it would result from repeated application of the distributivity transformation rule of disjunction over conjunction.

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.

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 specified 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 the result is a string or boolean, it is boxed in a corresponding class (String or Boolean) object, so the property can be attached to it.

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

Simplification functions might return the number of steps taken to do the simplification as additional information, depending on a steps option. This number of steps can be used to compare how close two expressions are to a given simplified form. Authors should not rely on particular values for the number of steps, as they could change without notice.

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.

• Basic Functions
  • logicSetOptions
  • logicParse
  • logicGetError
  • logicStringify
  • logicEvaluate
  • logicSort
• Expression Inspection
  • logicGetOperators
  • logicGetVariables
  • logicGetOperands
  • logicGetExpression
• Expression Search
  • logicFindOperator
  • logicFindExpression
  • logicFindRuleApplications
• Expression Transformations
  • logicApplyRule
  • logicApplyRules
  • logicCreateExpression
  • logicReplaceExpression
  • logicDeleteExpression
• Expression Simplifications
  • logicSimplifyNNF
  • logicSimplifyCNF
  • logicSimplifyDNF
  • logicSimplify
• Basic Expression Tests
  • logicValid
  • logicValued
  • logicSorted
• Expression Normal Form Tests
  • logicCheckTests
  • logicCheckNNF
  • logicCheckCNF
  • logicCheckDNF
• Expression Simplification Tests
  • logicSimplifiedNNF
  • logicSimplifiedCNF
  • logicSimplifiedDNF
  • logicSimplified
• Expression Comparison Tests
  • logicIdentical
  • logicEqual
  • logicEquivalent
  • logicAlwaysEqual
  • logicFindAlwaysEqualCounterexample

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

logicSetOptions(object = {})

• Arguments:
  • object - an option object containing settings as key-value pairs
• Result: an object containing the current set of options
• 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, including its original defaults.
• 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(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 a deep copy of it is returned.
• Usage Examples:
  logicParse('¬P ∨ ¬R ∧ Q') => a parse tree representing the expression

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(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(tree) => ¬P ∨ ¬R ∧ Q if tree is the tree generated from the same expression by logicParse
logicStringify(tree) => ¬P ∨ (¬R ∧ Q) for the same tree with strictParentheses set to true

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(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. The negation operator is not considered to contribute to expression complexity, although a negated expression is sorted after the same unnegated expression.
• Usage Examples:
  logicSort('¬R ∧ Q ∨ ¬P') => '¬P ∨ Q ∧ ¬R'
logicSort('¬((P ∨ Q) ∧ ¬R) ∧ S') => S ∧ ¬(¬R ∧ (P ∨ Q))

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

logicGetOperators(expression, {symbols = false, local = 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
  • local - an option boolean indicating search scope
• Result: an array of operator strings representing all operators in the expression
• Description: If local is false, it returns the 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. If local is true, it returns only the main operator of the given expression, again in a form according to the symbols option.
• 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']
logicGetOperators('¬R ∧ Q ∨ ¬P', {local: true}) => 'OR'
logicGetOperators('¬(¬P ∨ ¬Q)', {symbol: true, local: true}) => '¬'
logicGetOperators('P → Q → R ↔ P ∧ Q → R', {local: true}) => 'IFF'

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', 'R', 'P', 'Q', 'R']

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(expression, {start = 0, end = length + 1})

• Arguments:
  • expression - a logic expression to search, as a string or a tree
  • start - an option integer representing the start index in the expression string (defaulting to 0)
  • end - an option integer representing the end index in the expression string (defaulting to the end of the expression)
• Result: a subexpression as string or tree, representing the expression between the given indices
• Description: Returns a subexpression that represents the expression between the given indices of the whole expression string. It only works on expressions that result from parsing a string, without any other manipulations. The indices need to spread a proper subexpression, otherwise the result is null (but extra spaces around the subexpression are acceptable).
• Usage Examples:
  logicGetExpression('¬P ∧ Q ∨ ¬Q ∧ R') => '¬P ∧ Q ∨ ¬Q ∧ R'
logicGetExpression('¬P ∨ ¬Q ∨ (R ∧ S)', {start: 5}) => '¬Q ∨ (R ∧ S)'
logicGetExpression('(¬P ∧ Q) ∨ (¬Q ∧ R)', {start: 10, end: 19}) => '¬Q ∧ R'
logicGetExpression('¬R ∧ Q ∧ ¬P', {start: 0, end: 6}) => '¬R ∧ Q'
logicGetExpression('¬R ∧ Q ∧ ¬P', {start: 5, end: 7}) => 'Q'
logicGetExpression('¬R ∧ Q ∧ ¬P', {start: 5, end: 9}) => null

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(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: ...}, [String: 'P ∧ Q ∧ R'] {path: ...}]

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: ...}

logicFindRuleApplications(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:
  logicFindRuleApplications('¬(¬P ∨ ¬Q)', 'deMorgan') => ['¬(¬P ∨ ¬Q)']
logicFindRuleApplications('¬(¬P ∨ ¬Q)', 'deMorgan', {reverse: true}) => ['¬P ∨ ¬Q']
logicFindRuleApplications('¬(¬P ∨ ¬Q)', 'deMorgan', {reverse: true, paths: true}) => [[String: '¬P ∨ ¬Q'] {path: ...}]
logicFindRuleApplications('P → Q → R ↔ P ∧ Q → R', 'implication') => ['P → Q → R', 'Q → R', 'P ∧ Q → R']

These functions perform specific transformations on given expressions.

logicApplyRule(expression, rule, subexpression = null, {reverse = false, index = undefined})

• Arguments:
  • expression - a logic expression to transform, as a string or a tree
  • rule - a rule name string to apply
  • subexpression - a subexpression occurrence as a string or tree
  • reverse - an option boolean indicating direction
  • index - an option integer representing the rule occurrence or subexpression index
• Result: an expression as a string or tree, representing the result of applying the given rule to one or more subexpressions in the given expression
• Description: Returns an expression that is the result of applying the rule in the given second argument to the expression in the first argument. reverse indicates whether the rule is applied in the 'reverse' direction. If subexpression is present, the rule will be applied on occurrences of it as long as it is a proper subexpression of the given expression. If index is also present, it selects the occurrence of subexpression to apply the rule to. If index is missing, the subexpression can contain path information to select which occurrence to target. If neither index or a path are present, all occurrences of the subexpression in the given expression will have the rule applied to them. If subexpression is missing, index indicates which occurrence of the rule in the given expression should be replaced. If index and subexpression are both missing, all occurrences of the rule are replaced. If rule is missing or the rule cannot be found, or the subexpression cannot be found, it returns the given expression unchanged.
• Usage Examples:
  logicApplyRule('P → Q → R ↔ P ∧ Q → R', 'implication') => '¬P ∨ (¬Q ∨ R) ↔ ¬(P ∧ Q) ∨ R'
logicApplyRule('P → Q → R ↔ P ∧ Q → R', 'implication', {index: 0}) => '¬P ∨ (Q → R) ↔ P ∧ Q → R'
logicApplyRule('P → Q → R ↔ P ∧ Q → R', 'implication', {index: 1}) => 'P → ¬Q ∨ R ↔ P ∧ Q → R'
logicApplyRule('P → Q → R ↔ P ∧ Q → R', 'implication', {index: 2}) => 'P → Q → R ↔ ¬(P ∧ Q) ∨ R'
logicApplyRule('P → Q → R ↔ Q → R', 'implication', 'Q → R') => 'P → ¬Q ∨ R ↔ ¬Q ∨ R' logicApplyRule('P → Q → R ↔ Q → R', 'implication', 'Q → R', {index: 0}) => 'P → ¬Q ∨ R ↔ Q → R'
logicApplyRule('P → Q → R ↔ Q → R', 'implication', 'Q → R', {index: 1}) => 'P → Q → R ↔ ¬Q ∨ R'
logicApplyRule('P → Q → R ↔ Q → R', 'implication', [String: 'Q → R'] {path: ...}) => 'P → ¬Q ∨ R ↔ Q → R'

logicApplyRules(expression, rules = [], {reverse = false, local = false})

• Arguments:
  • expression - a logic expression to transform, as a string or a tree
  • rules - a rule name string or an array of rule names to apply
  • reverse - an option boolean indicating direction
  • local - 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. local indicates whether the rules are applied only to the main operator in the expression rather than to the whole expression. So if it is missing, the rules are applied to the whole expression. If rules is missing or empty, it returns the expression unchanged.
• Usage Examples:
  logicApplyRules('¬(¬P ∨ ¬Q)', 'deMorgan') => '¬¬P ∧ ¬¬Q'
logicApplyRules('¬(¬P ∨ ¬Q)', 'deMorgan', {reverse: true, global: true}) => '¬¬(P ∧ Q)'
logicApplyRules('¬(¬P ∨ ¬Q)', ['deMorgan', 'doubleNegation'], {global: true}) => 'P ∧ Q'
logicApplyRules('P → Q → R ↔ P ∧ Q → R', 'implication', {global: true}) => '¬P ∨ (¬Q ∨ R) ↔ ¬(P ∧ Q) ∨ R'

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(expression, oldsubexpression, newsubexpression, {index = undefined})

• 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 an 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 and index is undefined, the function will replace all occurrences of the oldsubexpression with newsubexpression.
• 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'
logicReplaceExpression('P ∨ Q ∨ P ∧ S', 'P', 'V ∧ W') => 'V ∧ W ∨ Q ∨ (V ∧ W) ∧ S'

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

• 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 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 and index is undefined, the function will delete all occurrences of the subexpression.
• Usage Examples:
  logicDeleteExpression('P ∨ Q ∨ P ∧ S', 'P', {index: 0}) => 'Q ∨ P ∧ S'
logicDeleteExpression('P ∨ Q ∨ P ∧ S', 'P', {index: 1}) => 'P ∨ Q ∨ S'
logicDeleteExpression('P ∨ Q ∨ P ∧ S', 'P') => 'Q ∨ S'

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(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(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(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}

logicSimplify(expression, {steps = false, flat = 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
  • flat - an option boolean indicating whether flat expressions should be preferred over shorter ones
• Result: a normal form expression equivalent to the given expression, as a string or tree
• Description: Returns an expression that represents the given expression reduced to one of the normal forms and simplified. The chosen normal form is the 'simplest' one, where 'simplest' is defined as having the lowest number of binary operators. However if flat is true a flatter DNF or CNF expression will be preferred over a deeper NNF expression. If steps is true, then the result will add a steps field that counts the number of steps in the simplification process.
• Usage Examples:
  logicSimplify('¬((P ∨ Q) ∧ ¬R) ∧ S') => S ∧ (R ∨ ¬P ∧ ¬Q)
logicSimplify('¬((P ∨ Q) ∧ ¬R) ∧ S', {flat: true}) => R ∧ S ∨ ¬P ∧ ¬Q ∧ S
logicSimplify('¬((P ∨ Q) ∧ ¬R) ∧ S', {steps: true, flat: true}) => [String: 'R ∧ S ∨ ¬P ∧ ¬Q ∧ S'] {steps: 16}

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(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(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(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

These functions test whether the given expression satisfies some given tests or 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.

logiCheckTests(expression, tests = [])

• Arguments:
  • expression - a logic expression to test as a string or a tree
  • tests - an array of tests to apply on the expression
• Result: a boolean value indicating if the given expression has passed all the given tests.
• Description: Returns a boolean value that indicates whether the given expression passes all the tests in the tests parameter. The list of currently implemented tests is described in section Tests.
• Usage Examples:
  logicCheckTests('¬(¬P ∨ ¬Q)', ['disjunctionOperator', 'atomicNegation']) => false
logicCheckTests('¬P ∨ ¬Q', ['disjunctionOperator', 'atomicNegation']) => true

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(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(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

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(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(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(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

logicSimplified(expression, {flat = false})

• Arguments:
  • expression - a logic expression to test as a string or a tree
  • flat - an option boolean indicating whether flat expressions should be preferred over shorter ones
• Result: a boolean value indicating if the given expression is simplified
• Description: Returns a boolean value that indicates whether the given expression is in one of the simplified normal forms. The test is done by reducing the expression to one of the normal forms, simplifying it, and comparing the result against the original parsed expression. It corresponds to function logicSimplify.
• Usage Examples:
  logicSimplified('S ∧ (R ∨ ¬P ∧ ¬Q)') => true
logicSimplified('S ∧ (R ∨ ¬P ∧ ¬Q)', {flat: true}) => false
logicSimplified('R ∧ S ∨ ¬P ∧ ¬Q ∧ S', {flat: true}) => true

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(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(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(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(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', {counterexample: true}) => [Boolean false] {counterexample: {P: true, Q: false}}

logicFindAlwaysEqualCounterexample(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:
  logicFindAlwaysEqualCounterexample('(P ∨ Q) ∧ ¬R', 'P ∧ ¬R ∨ Q ∧ ¬R') => undefined
logicFindAlwaysEqualCounterexample('¬(¬P ∨ ¬Q)', 'P ∨ Q') => {P: true, Q: false}