Home

The big idea

A platform that takes in easy-to-understand and easy-to-write logical statements and does fun things with them, like checking their consistency.

How though

Right now, two ways:

• The compiler, which is a jar file generated from this repo's CI that can be used like gcc or javac to change logic-app input into something sexy (see features section).
• A website, which is hostable by running the web sub-project. It has its own simple text-editor which does syntax highlighting, code warnings and compilation - all from the comfort of your browser.

(IDE integration is low priority)

Grammar

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

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

  • A sentence can be any first-order 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.
    • 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.

• One or more commands. Note: we have only tested with a single command per compilation thus far.

  • A command starts with the cmd marker 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
      • 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
      • 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: WIP
      • DIMACS CNF: WIP

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