diff --git a/dist/index.html b/dist/index.html index c552375..35fc453 100644 --- a/dist/index.html +++ b/dist/index.html @@ -74,6 +74,18 @@

Natural deduction

+ +
+ +
+

Sequent calculus

+ Sequent calculus was invented by Gentzen. +
Rules are easy to understand and proofs are easy to read
+
Very easy to (semi-)automatize
+
Proofs can have an exponential size
+
+ +
diff --git a/dist/sequentcalculus.html b/dist/sequentcalculus.html new file mode 100644 index 0000000..089c23f --- /dev/null +++ b/dist/sequentcalculus.html @@ -0,0 +1,355 @@ + + + + + + + + + + + + + + +

Pravda - sequent calculus

+ + On this page, you will learn about sequent calculus. Just like in natural deduction, sequent calculus is about manipulating sequents, but now there can be more than one formula on the right-hand side. For instance + p, q |- q, r + is a sequent, composed of: + + + Intuitively, Gamma |- Delta means that you can prove one of the formulas in Delta, based on the hypotheses in Gamma. The set Gamma can be empty, meaning you can prove one of the formulas in Delta without any hypotheses, as well as Delta which would mean the hypotheses in Gamma can prove false. + + This is only an introduction though, and sequent calculus is much richer than what we will see here! If you are interested, don't hesitate to take a look at the wikipedia page, as well as this wholesome document by David Baelde about more theoretical aspects of this proof system. + + +

In propositional logic

+ +

Axioms

+ There are three ways you can start a proof. First, and most intuitively, any sequent having the same proposition on the right and the left can be proved. + + + + + + Second, any sequent having false as an hypothesis can be proved: + + + + + Third, and symmetrically, having true as one of the conclusions is sufficient to be proved: + + + + +

Other rules

+ There are two rules for each connective of the propositional logic: a "left" one and and a "right" one, i.e. one if a formula having this connective as a root is an hypothesis or a conclusion. + +

Not

+ + + + + +

Or

+ + + + + +

And

+ + + + + +

Implication

+ + + + + +

Examples of proofs

+ + Proofs in sequent calculus are generally way simpler and more straightforward than in natural deduction. For instance, try to show p or (not p) (the law of excluded middle) in sequent calculus: + + + Try to prove the following De Morgan's law in sequent calculus: not (p or q) -> (not p) and (not q) + + + Try to prove the contraposition law in sqeuent calculus: (p -> q) -> (not q -> not p) + + + Try to prove Peirce's law: ((p -> q) -> p) -> p + + + Try to prove the definition of negation using implication: (not p -> (p -> bottom)) and ((p -> bottom) -> (not p)) + + + +

While the proofs are not that shorter compared to natural deduction, you can see that they are way more guided by the shape of the formulas. This is in part due to the subformula property of the sequent calculus: each formula appearing in the premisses is a subformula of another formula appearing in the conclusion of a rule.

+

This observation almost directly gives a proof search algorithm. Maybe this could tickle something in your brain if you are aware of some notions about complexity: we know for sure that the validity problem for propositional logic is coNP-complete, thus it would be an enormous breakthrough to show that it is in P, thanks to an hypothetical polynomial-time proof search algorithm.

+ However be reassured, this will not happen with sequent calculus, because the proof search algorithm we just found happens to have an exponential complexity, in the worst case. For example, try to prove the following (and quite boring) sequent: |- p and q, p and not q, not p and q, not p and not q + + +

First-order logic

+ +

First order rules

+ + Just like for propositional rules, we have a right and left rule for the existential and universal quantifier. This gives four rules in total. + +

Existential quantifier

+ When the formula is on the right, you can instantiate the variable with anything. + + + Note that the substitution of the variable x must not be ill-formed. For instance, the following is not a valid application of the rule: + + + However, you can always get around this issue by renaming linked variables: + + + + + However, on the left you must keep the variable as it is. + + + Be careful, though! You cannot apply this rule with a variable appearing free anywhere in the premisse sequent: + + +

Universal quantifier

+ The rules and restrictions are symmetric here: + + + + + + +

First examples of first-order proofs

+ + Try to prove the following formula: (forall x P(x)) -> (exists x P(x)) + + + Try to prove the distributy of the universal quantifier on conjunctions: forall x (P(x) and Q(x)) -> (forall x P(x)) and (forall x Q(x)) + + + Try to prove the duality of the existential and universal quantifiers: not (forall x P(x)) -> exists x (not P(x)) + + + Though those rules can seem satisfying, they are not sufficient to prove everything. Take a look at the following formula: exists x (forall y (P(y) -> P(x))). When we try to prove it using only the previous rules, we fail quite quickly: + + + But this formula is indeed valid (try to convince yourself of this!). A way to solve this problem is to add new structural rules, named contraction rules. + +

Contraction rules

+ As before, there is a left contraction rule as well as a right one. They are pretty straightforward: + + + + + Note that their introduction completely shatters any hope to get a proof search algorithm for first-order sequents, since it's a priori very hard to know when to apply them, and how many times. This was to be expected though, since first-order logic is not decidable. + +

First-order proofs using contraction rules

+ + Now equipped with those new rules, try to prove the previous formula: exists x (forall y (P(y) -> P(x))) (tip: you only have to apply contraction once!) + + + + Try to prove the drinking person's paradox: in a bar, there is always a person such that if this person drinks, everyone drinks. + + +

Sandbox

+ + In the following box, you can write any proof you want: + + + + + + diff --git a/dist/src/parser/parserSequent.js b/dist/src/parser/parserSequent.js new file mode 100644 index 0000000..44c66a7 --- /dev/null +++ b/dist/src/parser/parserSequent.js @@ -0,0 +1,1897 @@ +/* + * Generated by PEG.js 0.10.0. + * + * http://pegjs.org/ + */ + +(function(root, factory) { + if (typeof define === "function" && define.amd) { + define([], factory); + } else if (typeof module === "object" && module.exports) { + module.exports = factory(); + } else { + root.FormulaParser = factory(); + } +})(this, function() { +"use strict"; + +function peg$subclass(child, parent) { + function ctor() { this.constructor = child; } + ctor.prototype = parent.prototype; + child.prototype = new ctor(); +} + +function peg$SyntaxError(message, expected, found, location) { + this.message = message; + this.expected = expected; + this.found = found; + this.location = location; + this.name = "SyntaxError"; + + if (typeof Error.captureStackTrace === "function") { + Error.captureStackTrace(this, peg$SyntaxError); + } +} + +peg$subclass(peg$SyntaxError, Error); + +peg$SyntaxError.buildMessage = function(expected, found) { + var DESCRIBE_EXPECTATION_FNS = { + literal: function(expectation) { + return "\"" + literalEscape(expectation.text) + "\""; + }, + + "class": function(expectation) { + var escapedParts = "", + i; + + for (i = 0; i < expectation.parts.length; i++) { + escapedParts += expectation.parts[i] instanceof Array + ? classEscape(expectation.parts[i][0]) + "-" + classEscape(expectation.parts[i][1]) + : classEscape(expectation.parts[i]); + } + + return "[" + (expectation.inverted ? "^" : "") + escapedParts + "]"; + }, + + any: function(expectation) { + return "any character"; + }, + + end: function(expectation) { + return "end of input"; + }, + + other: function(expectation) { + return expectation.description; + } + }; + + function hex(ch) { + return ch.charCodeAt(0).toString(16).toUpperCase(); + } + + function literalEscape(s) { + return s + .replace(/\\/g, '\\\\') + .replace(/"/g, '\\"') + .replace(/\0/g, '\\0') + .replace(/\t/g, '\\t') + .replace(/\n/g, '\\n') + .replace(/\r/g, '\\r') + .replace(/[\x00-\x0F]/g, function(ch) { return '\\x0' + hex(ch); }) + .replace(/[\x10-\x1F\x7F-\x9F]/g, function(ch) { return '\\x' + hex(ch); }); + } + + function classEscape(s) { + return s + .replace(/\\/g, '\\\\') + .replace(/\]/g, '\\]') + .replace(/\^/g, '\\^') + .replace(/-/g, '\\-') + .replace(/\0/g, '\\0') + .replace(/\t/g, '\\t') + .replace(/\n/g, '\\n') + .replace(/\r/g, '\\r') + .replace(/[\x00-\x0F]/g, function(ch) { return '\\x0' + hex(ch); }) + .replace(/[\x10-\x1F\x7F-\x9F]/g, function(ch) { return '\\x' + hex(ch); }); + } + + function describeExpectation(expectation) { + return DESCRIBE_EXPECTATION_FNS[expectation.type](expectation); + } + + function describeExpected(expected) { + var descriptions = new Array(expected.length), + i, j; + + for (i = 0; i < expected.length; i++) { + descriptions[i] = describeExpectation(expected[i]); + } + + descriptions.sort(); + + if (descriptions.length > 0) { + for (i = 1, j = 1; i < descriptions.length; i++) { + if (descriptions[i - 1] !== descriptions[i]) { + descriptions[j] = descriptions[i]; + j++; + } + } + descriptions.length = j; + } + + switch (descriptions.length) { + case 1: + return descriptions[0]; + + case 2: + return descriptions[0] + " or " + descriptions[1]; + + default: + return descriptions.slice(0, -1).join(", ") + + ", or " + + descriptions[descriptions.length - 1]; + } + } + + function describeFound(found) { + return found ? "\"" + literalEscape(found) + "\"" : "end of input"; + } + + return "Expected " + describeExpected(expected) + " but " + describeFound(found) + " found."; +}; + +function peg$parse(input, options) { + options = options !== void 0 ? options : {}; + + var peg$FAILED = {}, + + peg$startRuleFunctions = { Sequent: peg$parseSequent }, + peg$startRuleFunction = peg$parseSequent, + + peg$c0 = "|-", + peg$c1 = peg$literalExpectation("|-", false), + peg$c2 = function(args1, args2) { + return {type: "sequent", args: [args1, args2]};}, + peg$c3 = ",", + peg$c4 = peg$literalExpectation(",", false), + peg$c5 = "", + peg$c6 = function(phi, tail) { + let args = [phi]; + tail.forEach(function(element) {args.push(element[3]); }); + return {type: "list", args: args};}, + peg$c7 = "Theta", + peg$c8 = peg$literalExpectation("Theta", false), + peg$c9 = "Gamma+", + peg$c10 = peg$literalExpectation("Gamma+", false), + peg$c11 = "Gamma", + peg$c12 = peg$literalExpectation("Gamma", false), + peg$c13 = "Sigma", + peg$c14 = peg$literalExpectation("Sigma", false), + peg$c15 = "Delta+", + peg$c16 = peg$literalExpectation("Delta+", false), + peg$c17 = "Delta", + peg$c18 = peg$literalExpectation("Delta", false), + peg$c19 = function() { + return text()}, + peg$c20 = function() {return {type: "list", args: []}; }, + peg$c21 = "exists", + peg$c22 = peg$literalExpectation("exists", false), + peg$c23 = function(x, phi) { + return {type: "exists", args: [x, phi]}; + }, + peg$c24 = "forall", + peg$c25 = peg$literalExpectation("forall", false), + peg$c26 = function(x, phi) { + return {type: "forall", args: [x, phi]}; + }, + peg$c27 = "->", + peg$c28 = peg$literalExpectation("->", false), + peg$c29 = function(phi, psi) { + return {type: "->", args: [phi, psi]}; + }, + peg$c30 = "or", + peg$c31 = peg$literalExpectation("or", false), + peg$c32 = function(phi, tail) { + let args = [phi]; + tail.forEach(function(element) {args.push(element[3]); }); + if(args.length == 1) + return args[0] + else + return {type: "or", args: args}; + }, + peg$c33 = "and", + peg$c34 = peg$literalExpectation("and", false), + peg$c35 = function(phi, tail) { + let args = [phi]; + tail.forEach(function(element) {args.push(element[3]); }); + if(args.length == 1) + return args[0] + else + return {type: "and", args: args}; + }, + peg$c36 = "(", + peg$c37 = peg$literalExpectation("(", false), + peg$c38 = ")", + peg$c39 = peg$literalExpectation(")", false), + peg$c40 = function(phi) { return phi; }, + peg$c41 = "not", + peg$c42 = peg$literalExpectation("not", false), + peg$c43 = function(phi) { + return {type: "not", args: [phi]}; + }, + peg$c44 = "bottom", + peg$c45 = peg$literalExpectation("bottom", false), + peg$c46 = "false", + peg$c47 = peg$literalExpectation("false", false), + peg$c48 = function() {return {type: "false", args: []};}, + peg$c49 = "top", + peg$c50 = peg$literalExpectation("top", false), + peg$c51 = "true", + peg$c52 = peg$literalExpectation("true", false), + peg$c53 = function() {return {type: "true", args: []};}, + peg$c54 = "phi", + peg$c55 = peg$literalExpectation("phi", false), + peg$c56 = "psi", + peg$c57 = peg$literalExpectation("psi", false), + peg$c58 = "chi", + peg$c59 = peg$literalExpectation("chi", false), + peg$c60 = "eta", + peg$c61 = peg$literalExpectation("eta", false), + peg$c62 = function() {return text();}, + peg$c63 = function(p) { + return {type: "atomic", pred:p, args: []}; + }, + peg$c64 = function(p, args) { + return {type: "atomic", pred:p, args: args}; + }, + peg$c65 = function(term, tail) { + let args = [term]; + tail.forEach(function(element) {args.push(element[3]); }); + return args; + }, + peg$c66 = function(c) {return {type: "term", func:c, args: []};}, + peg$c67 = function(f, args) { + return {type: "term", func:f, args: args}; + }, + peg$c68 = "x", + peg$c69 = peg$literalExpectation("x", false), + peg$c70 = "y", + peg$c71 = peg$literalExpectation("y", false), + peg$c72 = "z", + peg$c73 = peg$literalExpectation("z", false), + peg$c74 = "u", + peg$c75 = peg$literalExpectation("u", false), + peg$c76 = "v", + peg$c77 = peg$literalExpectation("v", false), + peg$c78 = "x'", + peg$c79 = peg$literalExpectation("x'", false), + peg$c80 = "y'", + peg$c81 = peg$literalExpectation("y'", false), + peg$c82 = "z'", + peg$c83 = peg$literalExpectation("z'", false), + peg$c84 = "u'", + peg$c85 = peg$literalExpectation("u'", false), + peg$c86 = "v'", + peg$c87 = peg$literalExpectation("v'", false), + peg$c88 = function() { return text();}, + peg$c89 = "0", + peg$c90 = peg$literalExpectation("0", false), + peg$c91 = "1", + peg$c92 = peg$literalExpectation("1", false), + peg$c93 = "a", + peg$c94 = peg$literalExpectation("a", false), + peg$c95 = "b", + peg$c96 = peg$literalExpectation("b", false), + peg$c97 = "c", + peg$c98 = peg$literalExpectation("c", false), + peg$c99 = "d", + peg$c100 = peg$literalExpectation("d", false), + peg$c101 = "e", + peg$c102 = peg$literalExpectation("e", false), + peg$c103 = "a'", + peg$c104 = peg$literalExpectation("a'", false), + peg$c105 = "b'", + peg$c106 = peg$literalExpectation("b'", false), + peg$c107 = "c'", + peg$c108 = peg$literalExpectation("c'", false), + peg$c109 = "d'", + peg$c110 = peg$literalExpectation("d'", false), + peg$c111 = "e'", + peg$c112 = peg$literalExpectation("e'", false), + peg$c113 = "f", + peg$c114 = peg$literalExpectation("f", false), + peg$c115 = "g", + peg$c116 = peg$literalExpectation("g", false), + peg$c117 = "h", + peg$c118 = peg$literalExpectation("h", false), + peg$c119 = "f'", + peg$c120 = peg$literalExpectation("f'", false), + peg$c121 = "g'", + peg$c122 = peg$literalExpectation("g'", false), + peg$c123 = "h'", + peg$c124 = peg$literalExpectation("h'", false), + peg$c125 = "p", + peg$c126 = peg$literalExpectation("p", false), + peg$c127 = "q", + peg$c128 = peg$literalExpectation("q", false), + peg$c129 = "r", + peg$c130 = peg$literalExpectation("r", false), + peg$c131 = "s", + peg$c132 = peg$literalExpectation("s", false), + peg$c133 = "t", + peg$c134 = peg$literalExpectation("t", false), + peg$c135 = function() {return text(); }, + peg$c136 = "P", + peg$c137 = peg$literalExpectation("P", false), + peg$c138 = "Q", + peg$c139 = peg$literalExpectation("Q", false), + peg$c140 = "R", + peg$c141 = peg$literalExpectation("R", false), + peg$c142 = "S", + peg$c143 = peg$literalExpectation("S", false), + peg$c144 = "T", + peg$c145 = peg$literalExpectation("T", false), + peg$c146 = "U", + peg$c147 = peg$literalExpectation("U", false), + peg$c148 = "V", + peg$c149 = peg$literalExpectation("V", false), + peg$c150 = peg$otherExpectation("whitespace"), + peg$c151 = /^[ \t\n\r]/, + peg$c152 = peg$classExpectation([" ", "\t", "\n", "\r"], false, false), + + peg$currPos = 0, + peg$savedPos = 0, + peg$posDetailsCache = [{ line: 1, column: 1 }], + peg$maxFailPos = 0, + peg$maxFailExpected = [], + peg$silentFails = 0, + + peg$result; + + if ("startRule" in options) { + if (!(options.startRule in peg$startRuleFunctions)) { + throw new Error("Can't start parsing from rule \"" + options.startRule + "\"."); + } + + peg$startRuleFunction = peg$startRuleFunctions[options.startRule]; + } + + function text() { + return input.substring(peg$savedPos, peg$currPos); + } + + function location() { + return peg$computeLocation(peg$savedPos, peg$currPos); + } + + function expected(description, location) { + location = location !== void 0 ? location : peg$computeLocation(peg$savedPos, peg$currPos) + + throw peg$buildStructuredError( + [peg$otherExpectation(description)], + input.substring(peg$savedPos, peg$currPos), + location + ); + } + + function error(message, location) { + location = location !== void 0 ? location : peg$computeLocation(peg$savedPos, peg$currPos) + + throw peg$buildSimpleError(message, location); + } + + function peg$literalExpectation(text, ignoreCase) { + return { type: "literal", text: text, ignoreCase: ignoreCase }; + } + + function peg$classExpectation(parts, inverted, ignoreCase) { + return { type: "class", parts: parts, inverted: inverted, ignoreCase: ignoreCase }; + } + + function peg$anyExpectation() { + return { type: "any" }; + } + + function peg$endExpectation() { + return { type: "end" }; + } + + function peg$otherExpectation(description) { + return { type: "other", description: description }; + } + + function peg$computePosDetails(pos) { + var details = peg$posDetailsCache[pos], p; + + if (details) { + return details; + } else { + p = pos - 1; + while (!peg$posDetailsCache[p]) { + p--; + } + + details = peg$posDetailsCache[p]; + details = { + line: details.line, + column: details.column + }; + + while (p < pos) { + if (input.charCodeAt(p) === 10) { + details.line++; + details.column = 1; + } else { + details.column++; + } + + p++; + } + + peg$posDetailsCache[pos] = details; + return details; + } + } + + function peg$computeLocation(startPos, endPos) { + var startPosDetails = peg$computePosDetails(startPos), + endPosDetails = peg$computePosDetails(endPos); + + return { + start: { + offset: startPos, + line: startPosDetails.line, + column: startPosDetails.column + }, + end: { + offset: endPos, + line: endPosDetails.line, + column: endPosDetails.column + } + }; + } + + function peg$fail(expected) { + if (peg$currPos < peg$maxFailPos) { return; } + + if (peg$currPos > peg$maxFailPos) { + peg$maxFailPos = peg$currPos; + peg$maxFailExpected = []; + } + + peg$maxFailExpected.push(expected); + } + + function peg$buildSimpleError(message, location) { + return new peg$SyntaxError(message, null, null, location); + } + + function peg$buildStructuredError(expected, found, location) { + return new peg$SyntaxError( + peg$SyntaxError.buildMessage(expected, found), + expected, + found, + location + ); + } + + function peg$parseSequent() { + var s0, s1, s2, s3, s4, s5; + + s0 = peg$currPos; + s1 = peg$parseFormulaListVariable(); + if (s1 === peg$FAILED) { + s1 = peg$parseFormulaList(); + } + if (s1 !== peg$FAILED) { + s2 = peg$parse_(); + if (s2 !== peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c0) { + s3 = peg$c0; + peg$currPos += 2; + } else { + s3 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c1); } + } + if (s3 !== peg$FAILED) { + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + s5 = peg$parseFormulaListVariable(); + if (s5 === peg$FAILED) { + s5 = peg$parseFormulaList(); + } + if (s5 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c2(s1, s5); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + if (s0 === peg$FAILED) { + s0 = peg$parseFormula(); + } + + return s0; + } + + function peg$parseFormulaList() { + var s0, s1, s2, s3, s4, s5, s6, s7; + + s0 = peg$currPos; + s1 = peg$parseFormula(); + if (s1 !== peg$FAILED) { + s2 = []; + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 44) { + s5 = peg$c3; + peg$currPos++; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c4); } + } + if (s5 === peg$FAILED) { + s5 = peg$c5; + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseFormula(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + while (s3 !== peg$FAILED) { + s2.push(s3); + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 44) { + s5 = peg$c3; + peg$currPos++; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c4); } + } + if (s5 === peg$FAILED) { + s5 = peg$c5; + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseFormula(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } + if (s2 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c6(s1, s2); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + if (s0 === peg$FAILED) { + s0 = peg$parseEmptyList(); + } + + return s0; + } + + function peg$parseFormulaListVariable() { + var s0, s1; + + if (input.substr(peg$currPos, 5) === peg$c7) { + s0 = peg$c7; + peg$currPos += 5; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c8); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 6) === peg$c9) { + s0 = peg$c9; + peg$currPos += 6; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c10); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 5) === peg$c11) { + s0 = peg$c11; + peg$currPos += 5; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c12); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 5) === peg$c13) { + s0 = peg$c13; + peg$currPos += 5; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c14); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 6) === peg$c15) { + s0 = peg$c15; + peg$currPos += 6; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c16); } + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 5) === peg$c17) { + s1 = peg$c17; + peg$currPos += 5; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c18); } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c19(); + } + s0 = s1; + } + } + } + } + } + + return s0; + } + + function peg$parseEmptyList() { + var s0, s1; + + s0 = peg$currPos; + s1 = peg$parse_(); + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c20(); + } + s0 = s1; + + return s0; + } + + function peg$parseFormula() { + var s0, s1, s2, s3, s4, s5, s6, s7; + + s0 = peg$currPos; + if (input.substr(peg$currPos, 6) === peg$c21) { + s1 = peg$c21; + peg$currPos += 6; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c22); } + } + if (s1 !== peg$FAILED) { + s2 = peg$parse_(); + if (s2 !== peg$FAILED) { + s3 = peg$parseVariableSymbol(); + if (s3 !== peg$FAILED) { + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + s5 = peg$parseFormula(); + if (s5 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c23(s3, s5); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 6) === peg$c24) { + s1 = peg$c24; + peg$currPos += 6; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c25); } + } + if (s1 !== peg$FAILED) { + s2 = peg$parse_(); + if (s2 !== peg$FAILED) { + s3 = peg$parseVariableSymbol(); + if (s3 !== peg$FAILED) { + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + s5 = peg$parseFormula(); + if (s5 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c26(s3, s5); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + s1 = peg$parseFormula2(); + if (s1 !== peg$FAILED) { + s2 = peg$parse_(); + if (s2 !== peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c27) { + s3 = peg$c27; + peg$currPos += 2; + } else { + s3 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c28); } + } + if (s3 !== peg$FAILED) { + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + s5 = peg$parseFormula(); + if (s5 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c29(s1, s5); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + s1 = peg$parseFormula2(); + if (s1 !== peg$FAILED) { + s2 = []; + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c30) { + s5 = peg$c30; + peg$currPos += 2; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c31); } + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseFormula(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + while (s3 !== peg$FAILED) { + s2.push(s3); + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c30) { + s5 = peg$c30; + peg$currPos += 2; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c31); } + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseFormula(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } + if (s2 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c32(s1, s2); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } + } + } + + return s0; + } + + function peg$parseFormula2() { + var s0, s1, s2, s3, s4, s5, s6, s7; + + s0 = peg$currPos; + s1 = peg$parseFactor(); + if (s1 !== peg$FAILED) { + s2 = []; + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.substr(peg$currPos, 3) === peg$c33) { + s5 = peg$c33; + peg$currPos += 3; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c34); } + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseFormula(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + while (s3 !== peg$FAILED) { + s2.push(s3); + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.substr(peg$currPos, 3) === peg$c33) { + s5 = peg$c33; + peg$currPos += 3; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c34); } + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseFormula(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } + if (s2 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c35(s1, s2); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + + return s0; + } + + function peg$parseFactor() { + var s0, s1, s2, s3, s4, s5; + + s0 = peg$currPos; + if (input.charCodeAt(peg$currPos) === 40) { + s1 = peg$c36; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c37); } + } + if (s1 !== peg$FAILED) { + s2 = peg$parse_(); + if (s2 !== peg$FAILED) { + s3 = peg$parseFormula(); + if (s3 !== peg$FAILED) { + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 41) { + s5 = peg$c38; + peg$currPos++; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c39); } + } + if (s5 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c40(s3); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 3) === peg$c41) { + s1 = peg$c41; + peg$currPos += 3; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c42); } + } + if (s1 !== peg$FAILED) { + s2 = peg$parse_(); + if (s2 !== peg$FAILED) { + s3 = peg$parseFactor(); + if (s3 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c43(s3); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + if (s0 === peg$FAILED) { + s0 = peg$parseAtomicFormula(); + } + } + + return s0; + } + + function peg$parseAtomicFormula() { + var s0, s1, s2, s3, s4; + + s0 = peg$currPos; + if (input.substr(peg$currPos, 6) === peg$c44) { + s1 = peg$c44; + peg$currPos += 6; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c45); } + } + if (s1 === peg$FAILED) { + if (input.substr(peg$currPos, 5) === peg$c46) { + s1 = peg$c46; + peg$currPos += 5; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c47); } + } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c48(); + } + s0 = s1; + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 3) === peg$c49) { + s1 = peg$c49; + peg$currPos += 3; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c50); } + } + if (s1 === peg$FAILED) { + if (input.substr(peg$currPos, 4) === peg$c51) { + s1 = peg$c51; + peg$currPos += 4; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c52); } + } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c53(); + } + s0 = s1; + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 3) === peg$c54) { + s1 = peg$c54; + peg$currPos += 3; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c55); } + } + if (s1 === peg$FAILED) { + if (input.substr(peg$currPos, 3) === peg$c56) { + s1 = peg$c56; + peg$currPos += 3; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c57); } + } + if (s1 === peg$FAILED) { + if (input.substr(peg$currPos, 3) === peg$c58) { + s1 = peg$c58; + peg$currPos += 3; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c59); } + } + if (s1 === peg$FAILED) { + if (input.substr(peg$currPos, 3) === peg$c60) { + s1 = peg$c60; + peg$currPos += 3; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c61); } + } + } + } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c62(); + } + s0 = s1; + if (s0 === peg$FAILED) { + s0 = peg$currPos; + s1 = peg$parsePropositionSymbol(); + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c63(s1); + } + s0 = s1; + if (s0 === peg$FAILED) { + s0 = peg$currPos; + s1 = peg$parsePredicateSymbol(); + if (s1 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 40) { + s2 = peg$c36; + peg$currPos++; + } else { + s2 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c37); } + } + if (s2 !== peg$FAILED) { + s3 = peg$parseTermList(); + if (s3 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 41) { + s4 = peg$c38; + peg$currPos++; + } else { + s4 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c39); } + } + if (s4 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c64(s1, s3); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } + } + } + } + + return s0; + } + + function peg$parseTermList() { + var s0, s1, s2, s3, s4, s5, s6, s7; + + s0 = peg$currPos; + s1 = peg$parseTerm(); + if (s1 !== peg$FAILED) { + s2 = []; + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 44) { + s5 = peg$c3; + peg$currPos++; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c4); } + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseTerm(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + while (s3 !== peg$FAILED) { + s2.push(s3); + s3 = peg$currPos; + s4 = peg$parse_(); + if (s4 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 44) { + s5 = peg$c3; + peg$currPos++; + } else { + s5 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c4); } + } + if (s5 !== peg$FAILED) { + s6 = peg$parse_(); + if (s6 !== peg$FAILED) { + s7 = peg$parseTerm(); + if (s7 !== peg$FAILED) { + s4 = [s4, s5, s6, s7]; + s3 = s4; + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } else { + peg$currPos = s3; + s3 = peg$FAILED; + } + } + if (s2 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c65(s1, s2); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + + return s0; + } + + function peg$parseTerm() { + var s0, s1, s2, s3, s4; + + s0 = peg$parseVariableSymbol(); + if (s0 === peg$FAILED) { + s0 = peg$currPos; + s1 = peg$parseConstantSymbol(); + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c66(s1); + } + s0 = s1; + if (s0 === peg$FAILED) { + s0 = peg$currPos; + s1 = peg$parseFunctionSymbol(); + if (s1 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 40) { + s2 = peg$c36; + peg$currPos++; + } else { + s2 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c37); } + } + if (s2 !== peg$FAILED) { + s3 = peg$parseTermList(); + if (s3 !== peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 41) { + s4 = peg$c38; + peg$currPos++; + } else { + s4 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c39); } + } + if (s4 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c67(s1, s3); + s0 = s1; + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } else { + peg$currPos = s0; + s0 = peg$FAILED; + } + } + } + + return s0; + } + + function peg$parseVariableSymbol() { + var s0, s1; + + if (input.charCodeAt(peg$currPos) === 120) { + s0 = peg$c68; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c69); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 121) { + s0 = peg$c70; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c71); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 122) { + s0 = peg$c72; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c73); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 117) { + s0 = peg$c74; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c75); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 118) { + s0 = peg$c76; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c77); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c78) { + s0 = peg$c78; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c79); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c80) { + s0 = peg$c80; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c81); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c82) { + s0 = peg$c82; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c83); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c84) { + s0 = peg$c84; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c85); } + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 2) === peg$c86) { + s1 = peg$c86; + peg$currPos += 2; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c87); } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c88(); + } + s0 = s1; + } + } + } + } + } + } + } + } + } + + return s0; + } + + function peg$parseConstantSymbol() { + var s0, s1; + + if (input.charCodeAt(peg$currPos) === 48) { + s0 = peg$c89; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c90); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 49) { + s0 = peg$c91; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c92); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 97) { + s0 = peg$c93; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c94); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 98) { + s0 = peg$c95; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c96); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 99) { + s0 = peg$c97; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c98); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 100) { + s0 = peg$c99; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c100); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 101) { + s0 = peg$c101; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c102); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c103) { + s0 = peg$c103; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c104); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c105) { + s0 = peg$c105; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c106); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c107) { + s0 = peg$c107; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c108); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c109) { + s0 = peg$c109; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c110); } + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 2) === peg$c111) { + s1 = peg$c111; + peg$currPos += 2; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c112); } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c88(); + } + s0 = s1; + } + } + } + } + } + } + } + } + } + } + } + + return s0; + } + + function peg$parseFunctionSymbol() { + var s0, s1; + + if (input.charCodeAt(peg$currPos) === 102) { + s0 = peg$c113; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c114); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 103) { + s0 = peg$c115; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c116); } + } + if (s0 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 104) { + s0 = peg$c117; + peg$currPos++; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c118); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c119) { + s0 = peg$c119; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c120); } + } + if (s0 === peg$FAILED) { + if (input.substr(peg$currPos, 2) === peg$c121) { + s0 = peg$c121; + peg$currPos += 2; + } else { + s0 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c122); } + } + if (s0 === peg$FAILED) { + s0 = peg$currPos; + if (input.substr(peg$currPos, 2) === peg$c123) { + s1 = peg$c123; + peg$currPos += 2; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c124); } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c88(); + } + s0 = s1; + } + } + } + } + } + + return s0; + } + + function peg$parsePropositionSymbol() { + var s0, s1; + + s0 = peg$currPos; + if (input.charCodeAt(peg$currPos) === 112) { + s1 = peg$c125; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c126); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 113) { + s1 = peg$c127; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c128); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 114) { + s1 = peg$c129; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c130); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 115) { + s1 = peg$c131; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c132); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 116) { + s1 = peg$c133; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c134); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 117) { + s1 = peg$c74; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c75); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 118) { + s1 = peg$c76; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c77); } + } + } + } + } + } + } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c135(); + } + s0 = s1; + + return s0; + } + + function peg$parsePredicateSymbol() { + var s0, s1; + + s0 = peg$currPos; + if (input.charCodeAt(peg$currPos) === 80) { + s1 = peg$c136; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c137); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 81) { + s1 = peg$c138; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c139); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 82) { + s1 = peg$c140; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c141); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 83) { + s1 = peg$c142; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c143); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 84) { + s1 = peg$c144; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c145); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 85) { + s1 = peg$c146; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c147); } + } + if (s1 === peg$FAILED) { + if (input.charCodeAt(peg$currPos) === 86) { + s1 = peg$c148; + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c149); } + } + } + } + } + } + } + } + if (s1 !== peg$FAILED) { + peg$savedPos = s0; + s1 = peg$c135(); + } + s0 = s1; + + return s0; + } + + function peg$parse_() { + var s0, s1; + + peg$silentFails++; + s0 = []; + if (peg$c151.test(input.charAt(peg$currPos))) { + s1 = input.charAt(peg$currPos); + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c152); } + } + while (s1 !== peg$FAILED) { + s0.push(s1); + if (peg$c151.test(input.charAt(peg$currPos))) { + s1 = input.charAt(peg$currPos); + peg$currPos++; + } else { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c152); } + } + } + peg$silentFails--; + if (s0 === peg$FAILED) { + s1 = peg$FAILED; + if (peg$silentFails === 0) { peg$fail(peg$c150); } + } + + return s0; + } + + peg$result = peg$startRuleFunction(); + + if (peg$result !== peg$FAILED && peg$currPos === input.length) { + return peg$result; + } else { + if (peg$result !== peg$FAILED && peg$currPos < input.length) { + peg$fail(peg$endExpectation()); + } + + throw peg$buildStructuredError( + peg$maxFailExpected, + peg$maxFailPos < input.length ? input.charAt(peg$maxFailPos) : null, + peg$maxFailPos < input.length + ? peg$computeLocation(peg$maxFailPos, peg$maxFailPos + 1) + : peg$computeLocation(peg$maxFailPos, peg$maxFailPos) + ); + } +} + +return { + SyntaxError: peg$SyntaxError, + parse: peg$parse +}; + +}); diff --git a/dist/src/parser/parserSequent.peg b/dist/src/parser/parserSequent.peg new file mode 100644 index 0000000..953f80f --- /dev/null +++ b/dist/src/parser/parserSequent.peg @@ -0,0 +1,133 @@ +Sequent = args1: (FormulaListVariable / FormulaList) _ "|-" _ args2: (FormulaListVariable / FormulaList) { + return {type: "sequent", args: [args1, args2]};} / Formula + + + +FormulaList = phi: Formula tail:(_ ("," / "") _ Formula)* { + let args = [phi]; + tail.forEach(function(element) {args.push(element[3]); }); + return {type: "list", args: args};} + / EmptyList + + +FormulaListVariable = "Theta" / "Gamma+" / "Gamma" / "Sigma" / "Delta+" / "Delta" { +return text()} + + + +EmptyList = _ {return {type: "list", args: []}; } + + + +Formula + = + "exists" _ x:VariableSymbol _ phi: Formula { + return {type: "exists", args: [x, phi]}; + } + + / + + "forall" _ x:VariableSymbol _ phi: Formula { + return {type: "forall", args: [x, phi]}; + } + + / + + + phi: Formula2 _ ("->") _ psi: Formula { + return {type: "->", args: [phi, psi]}; + } + + / + + phi:Formula2 tail:(_ ("or") _ Formula)* { + let args = [phi]; + tail.forEach(function(element) {args.push(element[3]); }); + if(args.length == 1) + return args[0] + else + return {type: "or", args: args}; + } + + + +Formula2 + = + phi:Factor tail:(_ ("and") _ Formula)* { + let args = [phi]; + tail.forEach(function(element) {args.push(element[3]); }); + if(args.length == 1) + return args[0] + else + return {type: "and", args: args}; + } + + +Factor + = "(" _ phi:Formula _ ")" { return phi; } + + / + + ("not") _ phi:Factor { + return {type: "not", args: [phi]}; + } + / + AtomicFormula + + + +AtomicFormula = ("bottom" / "false") {return {type: "false", args: []};} + / + ("top" / "true") {return {type: "true", args: []};} + / + ("phi" / "psi" / "chi" / "eta") {return text();} + / + p:PropositionSymbol { + return {type: "atomic", pred:p, args: []}; +} / + p:PredicateSymbol "(" args: TermList ")" { + return {type: "atomic", pred:p, args: args}; +} + + + +TermList + = term:Term tail:( _ (",") _ Term)* { + let args = [term]; + tail.forEach(function(element) {args.push(element[3]); }); + return args; + } + + + + + +Term + = VariableSymbol / c: ConstantSymbol + {return {type: "term", func:c, args: []};} + / + f:FunctionSymbol "(" args: TermList ")" { + return {type: "term", func:f, args: args}; + } + + +VariableSymbol + = "x" / "y" / "z" / "u" / "v" / + "x'" / "y'" / "z'" / "u'" / "v'" { return text();} + +ConstantSymbol + = "0" / "1" / "a" / "b" / "c" / "d" / "e" / "a'" / "b'" / "c'" / "d'" / "e'" { return text();} + +FunctionSymbol + = "f" / "g" / "h" / "f'" / "g'" / "h'" { return text();} + + +PropositionSymbol + = ("p" / "q" / "r" / "s" / "t" / "u" / "v") {return text(); } + +PredicateSymbol + = ("P" / "Q" / "R" / "S" / "T" / "U" / "V") {return text(); } + + +_ "whitespace" + = [ \t\n\r]* diff --git a/src/Formula.ts b/src/Formula.ts index 3714e31..b5ba8f0 100644 --- a/src/Formula.ts +++ b/src/Formula.ts @@ -110,6 +110,21 @@ export class FormulaUtility { */ static not = (f: Formula) => { return { type: "not", args: [f] } }; + /** + * @param a formula of the form Q x. phi(x) + * @returns phi(x) + * */ + + static getQuantifierSub = (f: FormulaConstruction) => { return f.args[1]; } + + /** + * @param a formula of the form Q x. phi(x) + * @returns x + * */ + + static getQuantifierVar = (f: FormulaConstruction) => { return f.args[0]; } + + /** * @param phi an expression @@ -153,4 +168,4 @@ UnitTest.run("isFreeVariable", !FormulaUtility.isFreeVariable(stringToFormula("f UnitTest.run("isFreeVariable", !FormulaUtility.isFreeVariable("y", "x")); UnitTest.run("isFreeVariable", FormulaUtility.isFreeVariable(stringToFormula("P(x)"), "x")); UnitTest.run("isFreeVariable", !FormulaUtility.isFreeVariable(stringToFormula("P(y)"), "x")); -UnitTest.run("isFreeVariable", FormulaUtility.isFreeVariable(stringToFormula("P(y) and P(x)"), "x")); \ No newline at end of file +UnitTest.run("isFreeVariable", FormulaUtility.isFreeVariable(stringToFormula("P(y) and P(x)"), "x")); diff --git a/src/ProverComponent.ts b/src/ProverComponent.ts index e63b1fe..9a098a8 100644 --- a/src/ProverComponent.ts +++ b/src/ProverComponent.ts @@ -3,6 +3,7 @@ import { Proof, stringToProof, Justification } from "./Proof.js"; import { ResolutionProofSystem } from "./ResolutionProofSystem.js"; import { HilbertProofSystem } from './HilbertProofSystem.js'; import { NaturalDeduction } from './NaturalDeduction.js'; +import { SequentCalculus } from './SequentCalculus.js'; import { stringToFormula, Formula, formulaToLaTeX } from './Formula.js'; import * as Utils from "./Utils.js"; import { proofToProofTreeLaTeX, askForMathJAX } from './LaTeX.js'; @@ -77,6 +78,7 @@ export class ProverComponent { case "ResolutionProofSystem": proofSystem = new ResolutionProofSystem(); break; case "HilbertProofSystem": proofSystem = new HilbertProofSystem(); break; case "NaturalDeduction": proofSystem = new NaturalDeduction(); break; + case "SequentCalculus": proofSystem = new SequentCalculus(); break; default: proofSystem = new HilbertProofSystem(); } diff --git a/src/SeqCalcUtils.ts b/src/SeqCalcUtils.ts new file mode 100644 index 0000000..d876f02 --- /dev/null +++ b/src/SeqCalcUtils.ts @@ -0,0 +1,211 @@ +import * as Utils from "./Utils.js" +import { patternMatchingFormula } from "./PatternMatching.js"; +import { FormulaUtility } from "./Formula.js"; +import { ProofSystem } from "./ProofSystem.js"; + +/** + * + * @param gammaHyp + * @param deltaHyp + * @param gammaConcl + * @param deltaConcl + * @returns true iff gammaHyp = gammaConcl, A and deltaConcl = deltaHyp, not A + * */ +export function negRulePattern(gammaHyp: any[], deltaHyp: any[], + gammaConcl: any[], deltaConcl: any[]): boolean { + if (!Utils.includes(gammaHyp, gammaConcl) || gammaHyp.length != gammaConcl.length + 1) { return false; } + + let pFormula = { + type: "not", + args: Utils.multisetDifference(gammaHyp, gammaConcl) + }; + + return Utils.isMultisetPlusElement(deltaConcl, deltaHyp, pFormula); +} + +/** + * + * @param deltaHyp + * @param deltaConcl + * @param formulaType + * @returns true iff deltaHyp and deltaConcl are multisets of the form: + * delta, A, B and delta, formulaType(A, B) + */ +export function orRightRulePattern(deltaHyp: any[], deltaConcl: any[], formulaType: string): boolean { + + let formulas = Utils.multisetDifference(deltaHyp, deltaConcl); + if (formulas.length != 2 || deltaConcl.length + 1 != deltaHyp.length) { return false; } + + let pFormula = { + type: formulaType, + args: formulas + }; + + let pFormula2 = { + type: formulaType, + args: [formulas[1], formulas[0]] + }; + + return Utils.isMultisetPlusElement(deltaConcl, + Utils.multisetDifference(deltaHyp, formulas), pFormula) + || Utils.isMultisetPlusElement(deltaConcl, + Utils.multisetDifference(deltaHyp, formulas), pFormula2); +} + + +/** + * + * @param gammaHyp + * @param deltaHyp + * @param gammaConcl + * @param deltaConcl + * @param formulaType + * @returns true iff gammaHyp = gammaConc, A ; deltaHyp = delta, B ; + * and deltaConcl = delta, formulaType(A, B) + * */ + +export function implRightRulePattern(gammaHyp: any[], deltaHyp: any[], gammaConcl: any[], deltaConcl: any[], + formulaType: string) { + + let phiArray = Utils.multisetDifference(gammaHyp, gammaConcl); + let psiArray = Utils.multisetDifference(deltaHyp, deltaConcl); + if (phiArray.length != 1 || psiArray.length != 1) { return false; } + + let pFormula = { + type: formulaType, + args: phiArray.concat(psiArray) + }; + + + let b1 = Utils.isMultisetPlusElement(gammaHyp, gammaConcl, phiArray[0]); + let b2 = Utils.isMultisetPlusElement(deltaHyp, + Utils.multisetDifference(deltaConcl, [pFormula]), psiArray[0]); + let b3 = Utils.isMultisetPlusElement(deltaConcl, + Utils.multisetDifference(deltaHyp, psiArray), pFormula); + + return b1 && b2 && b3; +} + +/** + * + * @param deltaHyp1 + * @param deltaHyp2 + * @param deltaConcl + * @return true iff deltaHyp1, deltaHyp2, deltaConcl are of the form delta, phi; delta, psi; + * delta, formulatype(phi, psi) + */ +export function orLeftRulePattern(deltaHyp1: any[], deltaHyp2: any[], deltaConcl: any[], formulaType: string) { + let phi = Utils.multisetDifference(deltaHyp1, deltaConcl); + let psi = Utils.multisetDifference(deltaHyp2, deltaConcl); + if (phi.length != 1 || psi.length != 1) { return false; } + + let pFormula = { + type: formulaType, + args: phi.concat(psi) + }; + + let b1 = Utils.isMultisetPlusElement(deltaConcl, + Utils.multisetDifference(deltaHyp1, phi), pFormula); + let b2 = Utils.isMultisetPlusElement(deltaConcl, + Utils.multisetDifference(deltaHyp2, psi), pFormula); + + return b1 && b2; +} + +/** + * + * @param gammaHyp1 + * @param gammaHyp2 + * @param deltaHyp2 + * @param gammaConcl + * @param deltaConcl + * @param array + * @return true iff: + * gammaHyp1 |- deltaConcl and gammaHyp2 |- deltaHyp2 are sequents of the form + * gamma U {phi} |- delta, gamma |- delta U {psi} + * and gammaConcl |- deltaConcl is a sequent of the form gamma U {formulaType(psi, phi)} |- delta + */ +export function implLeftRulePattern(gammaHyp1: any[], + gammaHyp2: any[], deltaHyp2: any[], + gammaConcl: any[], deltaConcl: any[], formulaType: string): boolean { + + if (gammaHyp1.length != gammaConcl.length) { return false; } + + let phi = Utils.multisetDifference(gammaHyp1, gammaConcl); + let psi = Utils.multisetDifference(deltaHyp2, deltaConcl); + if (phi.length != 1 || psi.length != 1) { return false; } + + let pFormula = { + type: formulaType, + args: psi.concat(phi) + }; + + let b1 = Utils.isMultisetPlusElement(deltaHyp2, deltaConcl, psi[0]); + let b2 = Utils.isMultisetPlusElement(gammaConcl, + Utils.multisetDifference(gammaHyp1, phi), pFormula); + let b3 = Utils.isMultisetPlusElement(gammaConcl, gammaHyp2, pFormula); + return b1 && b2 && b3; +} + +/** + * + * @param gammaHyp + * @param gammaConcl + * @param deltaHyp + * @param quantifier + * @param allowSubstitution + * @return There are two cases: + * - If allowSubstitution is true, then true iff gammaConcl = gamma, quantifier x. phi(x) and + * gammaHyp = gamma, phi(u) + * - If allowSubstitution is false, then true iff gammaConcl = gamma, quantifier x. phi(x) and + * gammaHyp = gamma, phi(x) with x not being free in gammaHyp or deltaHyp + * */ +export function quantifierRulePattern(gammaHyp: any[], gammaConcl: any[], deltaHyp: any[], + quantifier: string, allowSubstitution: boolean): any { + + let pFormulaArray = Utils.multisetDifference(gammaConcl, gammaHyp); + if (pFormulaArray.length != 1) { return false; } + + let pFormula = pFormulaArray[0]; + if (pFormula.type != quantifier) { return false; } + // We know pFormula is Qx. phi(x) + + let phi = FormulaUtility.getQuantifierSub(pFormula); + if (allowSubstitution) { + let psiArray = Utils.multisetDifference(gammaHyp, gammaConcl); + if (psiArray.length != 1) { return false; } + + let psi = psiArray[0]; + if (patternMatchingFormula(phi, psi)) return true; else return false; + } else { + let x = FormulaUtility.getQuantifierVar(pFormula); + + // x should not be a free variable of any formula in gammaHyp or deltaHyp + for (let f of Utils.multisetDifference(gammaHyp, [phi]).concat(deltaHyp)) { + if (FormulaUtility.isFreeVariable(f, x)) { + let s = (quantifier == "forall") ? "forall right" : "exists left"; + return ProofSystem.ruleIssue(s + " but variable " + x + " is not free"); + } + } + + return Utils.isMultisetPlusElement(gammaHyp, + Utils.multisetDifference(gammaConcl, pFormulaArray), phi); + } +} + +/** + * + * @param gammaHyp + * @param gammaConcl + * @returns true iff gammaHyp and gammaConcl are of the form gamma, phi, phi and gamma, phi + * respectively. + */ +export function contractionRulePattern(gammaHyp: any[], gammaConcl: any[]): boolean { + if (gammaHyp.length != gammaConcl.length + 1) { return false; } + + let phiArray = Utils.multisetDifference(gammaHyp, gammaConcl); + if (phiArray.length != 1) { return false; } + + let phi = phiArray[0]; + return Utils.contains(gammaConcl, phi); +} diff --git a/src/SequentCalculus.ts b/src/SequentCalculus.ts new file mode 100644 index 0000000..284affe --- /dev/null +++ b/src/SequentCalculus.ts @@ -0,0 +1,90 @@ +import { ProofSystem } from "./ProofSystem.js"; +import { axiomPattern, rule1Pattern, rule2Pattern } from "./PatternMatching.js"; +import * as Utils from "./Utils.js"; +import * as SCUtils from "./SeqCalcUtils.js"; + +export class SequentCalculus extends ProofSystem { + constructor() { + + super(); + + // Axioms + this.addRule0( + axiomPattern("axiom", "Gamma |- Delta", + (sub) => { + return Utils.isNotEmptyIntersection(sub["Gamma"].args, sub["Delta"].args); + })); + + this.addRule0( + axiomPattern("bottom left", "Gamma |- Delta", + (sub) => Utils.contains(sub["Gamma"].args, {type: "false", args: []})) + ); + + this.addRule0( + axiomPattern("top right", "Gamma |- Delta", + (sub) => Utils.contains(sub["Delta"].args, {type: "true", args: []})) + ); + + // Propositional rules + this.addRule1( + rule1Pattern("neg right", "Gamma+ |- Delta", "Gamma |- Delta+", + (sub) => SCUtils.negRulePattern(sub["Gamma+"].args, sub["Delta"].args, + sub["Gamma"].args, sub["Delta+"].args))); + + this.addRule1( + rule1Pattern("neg left", "Gamma |- Delta+", "Gamma+ |- Delta", + (sub) => SCUtils.negRulePattern(sub["Delta+"].args, sub["Gamma"].args, + sub["Delta"].args, sub["Gamma+"].args))); + + this.addRule1( + rule1Pattern("or right", "Gamma |- Delta", "Gamma |- Delta+", + (sub) => SCUtils.orRightRulePattern(sub["Delta"].args, sub["Delta+"].args, "or"))); + + this.addRule1( + rule1Pattern("and left", "Gamma+ |- Delta", "Gamma |- Delta", + (sub) => SCUtils.orRightRulePattern(sub["Gamma+"].args, sub["Gamma"].args, "and"))); + + this.addRule1( + rule1Pattern("impl right", "Gamma+ |- Delta", "Gamma |- Sigma", + (sub) => SCUtils.implRightRulePattern(sub["Gamma+"].args, sub["Delta"].args, + sub["Gamma"].args, sub["Sigma"].args, "->"))); + + this.addRule2(rule2Pattern("and right", "Gamma |- Theta", "Gamma |- Sigma", "Gamma |- Delta", + (sub) => SCUtils.orLeftRulePattern(sub["Theta"].args, sub["Sigma"].args, sub["Delta"].args, "and") + )); + + this.addRule2(rule2Pattern("or left", "Gamma |- Delta", "Theta |- Delta", "Sigma |- Delta", + (sub) => SCUtils.orLeftRulePattern(sub["Gamma"].args, sub["Theta"].args, sub["Sigma"].args, "or"))); + + + this.addRule2(rule2Pattern("impl left", "Gamma+ |- Delta", "Gamma |- Delta+", "Theta |- Delta", + (sub) => SCUtils.implLeftRulePattern(sub["Gamma+"].args, + sub["Gamma"].args, sub["Delta+"].args, + sub["Theta"].args, sub["Delta"].args, "->"))); + + // First order rules + this.addRule1(rule1Pattern("exists right", "Gamma |- Sigma", "Gamma |- Delta", + (sub) => SCUtils.quantifierRulePattern(sub["Sigma"].args, sub["Delta"].args, sub["Gamma"].args, + "exists", true))); + + this.addRule1(rule1Pattern("forall left", "Theta |- Delta", "Gamma |- Delta", + (sub) => SCUtils.quantifierRulePattern(sub["Theta"].args, sub["Gamma"].args, sub["Delta"].args, + "forall", true))); + + this.addRule1(rule1Pattern("forall right", "Gamma |- Sigma", "Gamma |- Delta", + (sub) => SCUtils.quantifierRulePattern(sub["Sigma"].args, sub["Delta"].args, sub["Gamma"].args, + "forall", false))); + + this.addRule1(rule1Pattern("exists left", "Theta |- Delta", "Gamma |- Delta", + (sub) => SCUtils.quantifierRulePattern(sub["Theta"].args, sub["Gamma"].args, sub["Delta"].args, + "exists", false))); + + // Structural rules + this.addRule1(rule1Pattern("contra left", "Gamma+ |- Delta", "Gamma |- Delta", + (sub) => SCUtils.contractionRulePattern(sub["Gamma+"].args, sub["Gamma"].args))); + + this.addRule1(rule1Pattern("contra right", "Gamma |- Delta+", "Gamma |- Delta", + (sub) => SCUtils.contractionRulePattern(sub["Delta+"].args, sub["Delta"].args))); + + } +} diff --git a/src/Utils.ts b/src/Utils.ts index b22d3a1..d08167d 100644 --- a/src/Utils.ts +++ b/src/Utils.ts @@ -68,6 +68,25 @@ export function isSetPlusElement(bigArray: any[], array: any[], element: any): b } +/** + * + * @param array1 + * @param array2 + * @return true iff array1 interesected with array2 is not empty + */ +export function isNotEmptyIntersection(array1: any[], array2: any[]): boolean { + for (let e of array1) { + if (contains(array2, e)) { + return true; + } + } + + return false; +} + +UnitTest.run("isNotEmptyIntersection", isNotEmptyIntersection(["p", "q"], ["p"])); +UnitTest.run("isNotEmptyIntersection", isNotEmptyIntersection(["p"], ["p"])); +UnitTest.run("isNotEmptyIntersection", !isNotEmptyIntersection(["q"], ["p"])); UnitTest.run("isSetPlusElement", isSetPlusElement(["p"], [], "p")); UnitTest.run("isSetPlusElement", isSetPlusElement(["p", "q"], ["p"], "q")); @@ -77,4 +96,60 @@ UnitTest.run("isSetPlusElement", !isSetPlusElement(["p", "q"], ["p"], "p")); export function setAdd(array: any[], element: any): void { if (!contains(array, element)) array.push(element); -} \ No newline at end of file +} + + +/** + * + * @param array + * @param element + * @returns Nothing, but removes one occurrence of element from array if it existed + */ +function remove(array: any[], element: any) { + let found = false; + let i = 0; + while (i < array.length && !found) { + if (same(element, array[i])) { + array.splice(i, 1); + found = true; + } + i++; + } +} + +/** + * + * @param bigArray + * @param array + * @returns An array containing all elements in [bigArray] that are not in [array] + */ +export function multisetDifference(bigArray: any[], array: any[]): any[] { + let newArray = bigArray.slice(); // Copy of bigArray + for (let e of array) { + remove(newArray, e); + } + + return newArray +} + +/** + * + * @param bigArray + * @param array + * @param element + * @return true iff bigArray = array U {element} + */ +export function isMultisetPlusElement(bigArray: any[], array: any[], element: any): boolean { + if (bigArray.length != array.length + 1) + return false; + + let bigCount = bigArray.filter(x => same(x, element)).length; + let count = array.filter(x => same(x, element)).length; + + if (bigCount != count + 1) { return false; } + + return includes(bigArray, array); +} + +UnitTest.run("setMinus1", multisetDifference(["p", "q"], ["q"])[0] == "p"); +UnitTest.run("setMinus2", multisetDifference(["p", "p"], ["p"])[0] == "p");