Grammar

Grammar spec

Logic-app input files must have the .logic extension, and follow this format:

• One or more propositions. A proposition starts with the prop keyword followed by a logical sentence.

  • A sentence can be any propositional logical expression, with terminals and operators.

    • Terminals (AKA atoms) are the smallest logical unit. A terminal can either be a boolean literal or a boolean variable.
      • A boolean literal is either T or F (symbol variant) or True or False (reserved word variant).
      • A boolean variable can be named anything you can name a Java variable. That means single letters (excluding T and F) or longer form words with optional underscores. In testing and in documentation we typically use single letters because this is the norm in logic.
    • Supported operators:

    Class	Resword	Symbol
    Conjunction	and	&
    Disjunction	or	|
    Negation	not	~
    Implication	implies	->
    Equivalence	iff	<->

    • Notably "nand" and "xor" operations are not directly supported. They can be indirectly crafted as such:

      ~(A & B)               # nand
      (A | B) & (~A | ~B)    # xor
      

    • Use of parentheses to indicate order of operations is recommended, but there is a grammar-level order of operations that holds otherwise:

      1. Negation
      2. Conjunction
      3. Disjunction
      4. Implication
      5. Equivalence.

• A command. More than one command may be specified, but use cases for this are limited.

  • A command starts with the cmd keyword and is followed by a controlled-natural-language-style command. Supported commands:
    • just parse: Output nothing. Useful if you just want to check the syntax and validation of your input.
    • translate to [variant]. Supported variants:
      • reserved word variant: Changes all the operators and boolean literals to their reserved-word-variant equivalents. E.g. -> will change to implies.
      • symbol variant: Changes all the operators and boolean literals to their symbol-variant equivalents. E.g. implies will change to ->.
    • convert to [conversion]. Supported conversions:
      • NNF: Change each proposition to Negation Normal Form. That is, the sentence will only consist of & and | operators, and ~ operators will only appear directly next to terminals.
      • CNF: Conjunctive Normal Form. I.e. NNF, and & operators will always be logically higher than | operators.
      • DIMACS CNF: Special kind of text format that can be read by most SAT solvers. Simplified spec here.
    • solve [what]. Supported solvings:
      • satisfiability: See SAT Solving wiki page.

• Any number of configuration items.

  • A config item starts with the config keyword, followed by the config key, an = character, and then the value in string format. E.g.:

  config solver="sat4j"
  

  • The string may be specified using single or double quotes.
  • See the config wiki entry for valid config keys and values.

• Optionally, comments! Comments start with # and run to the end of the line.

• The grammar is whitespace-blind, so you can place multiple propositions and commands on the same line. For obvious reasons, this is not recommended.

Variants

The grammar works with two variants:

• The symbol variant, which uses symbols as operators and the short-form boolean literals, e.g. ->, &, T.
• The reserved word variant, which uses words as operators and the long-form boolean literals, e.g. implies, and, True.

Mixing these variants is allowed, but will trigger warnings.