First-order logic parser file for PEG.js, can handle weighted formulas of the form FORMULA ; WEIGHT.

fol.pegjs

{
  function getTerms(t, ts) {
    if (t) {
      var arr = [];
      for (var i = 0; i < ts.length; ++i) {
        arr.push(ts[i][2]);
      }
      return [t].concat(arr);
    }
    return [];
  }
  function buildName(fst, rest) {
    return fst + rest.join("");
  }
  function getQual(q) {
    return q == "A." || q.toLowerCase() == "forall" || q == "∀"? "forall" : "exists";
  }
}

start = formula

// Patterns to match logic connectives
matchNeg  = "not"i / "!" / "~" / "¬"
matchQual = "A." / "forall"i / "∀" / "exists"i / "E." / "∃"
matchIff  = "iff"i / "<=>" / "⇔"
matchXor  = "xor"i / "⊕" / "⊻"
matchImp  = "implies"i / "=>" / "⇒"
matchOr   = "or"i / "v" / "∨"
matchAnd  = "and"i / "∧"

// Formula
formula = wformula / uformula

// Weighted formula
wformula =
  fm:negq _ ";" _ weight:[0-9.]+ {
    return { formula: fm, weight: Number(weight.join("")) };
  }

// Unweighted formula
uformula = fm:negq { return { formula: fm }; }

// Logical negation for qualifiers
negq  = matchNeg _ x:negq { return { not: x }; } / qual

// Universal & existential qualifications
qual = q:matchQual _ v:variable vs:("," _ variable)* _ ":"? _ fm:negq {
    return { qualifier: { kind: getQual(q), variables: getTerms(v, vs), formula: fm } };
  } / iff

// Material equivalence
iff  = x:xor _ matchIff _ y:iff { return { binop: { kind: "iff", left: x, right: y } }; } / xor

// Exclusive disjunction
xor = x:imp _ matchXor _ y:xor { return { binop: { kind: "xor", left: x, right: y } }; } / imp

// Logical implication
imp  = x:or _ matchImp _ y:imp { return { binop: { kind: "implies", left: x, right: y } }; } / or

// Disjunction
or = x:and _ matchOr _ y:or  { return { binop: { kind: "or", left: x, right: y } }; } / and

// Conjunction
and  = x:neg _ matchAnd _ y:and { return { binop: { kind: "and", left: x, right: y } }; } / neg

// Logical negation
neg  = matchNeg _ x:neg { return { not: x }; } / atomic

atomic
  = identity
  / pred
  / "⊤" { return { predicate: { name: "true" } }; }
  / "⊥" { return { predicate: { name: "false" } }; }
  / "(" _ expr:negq _ ")" { return expr; }
  / "[" _ expr:negq _ "]" { return expr; }

// Syntactic sugar for the identity predicates:
identity =
  t0:term _ s:("==" / "=" / "!=" / "/=") _ t1:term {
    var f = { predicate: { name: "equals", args: [t0, t1] } };
    return s == "!=" || s == "/="? { not: f } : f;
  }

pred =
  fst:[a-zA-Z] txt:[a-zA-Z0-9]* ts:terms? {
    return { predicate: { name: (fst + txt.join("")), args: (ts? ts : undefined) } };
  }

terms = "(" _ t:term? ts:("," _ term)* _ ")" { return getTerms(t, ts); }

functerm = fst:[a-zA-Z] txt:[a-zA-Z0-9]* "(" _ t:term? ts:("," _ term)* _ ")" {
    return { kind: "function", name: buildName(fst, txt), args: getTerms(t, ts) };
  }
variable = fst:[a-z] txt:[a-zA-Z0-9]* { return { kind: "variable", name: buildName(fst, txt) }; }
constant = txt:[a-zA-Z0-9]+ { return { kind: "constant", name: txt.join("") }; }

term = functerm / variable / constant

_  = [ \t\r\n]* // optional whitespace

__ = [ \t\r\n]+ // mandatory whitespace