From d75a8510cb9356f996c363ac0ae1b7f25139ea3e Mon Sep 17 00:00:00 2001 From: Jenny Gao Date: Sun, 26 Mar 2023 20:02:13 -0400 Subject: [PATCH 01/54] =?UTF-8?q?add=20=E2=8A=A4=20and=20=E2=8A=A5?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Jody Sunray <55996087+jssunray34@users.noreply.github.com> --- userguide.md | 2 ++ views/index.pug | 8 ++++++++ 2 files changed, 10 insertions(+) diff --git a/userguide.md b/userguide.md index 6de9325..b2ad00f 100644 --- a/userguide.md +++ b/userguide.md @@ -32,6 +32,8 @@ Symbol|Options [Equivalence](https://en.wikipedia.org/wiki/If_and_only_if)|`iff` `equiv` `↔` `%` `<->` [Universal Quantifier](https://en.wikipedia.org/wiki/Universal_quantification)|`forall` `∀` [Existential Quantifier](https://en.wikipedia.org/wiki/Existential_quantification)|`exists` `∃` +[Tautology](https://en.wikipedia.org/wiki/Tautology_(logic))|`⊤` +[Contradition](https://en.wikipedia.org/wiki/Contradiction)|`⊥` Open Branch|`◯` Closed Branch|`×` diff --git a/views/index.pug b/views/index.pug index 7e087f6..bc62704 100644 --- a/views/index.pug +++ b/views/index.pug @@ -257,6 +257,14 @@ html(lang='en') td ∃ td substitution-recorder(symbol='∃' default='/') + tr + td ⊤ + td + substitution-recorder(symbol='⊤' default='T') + tr + td ⊥ + td + substitution-recorder(symbol='⊥' default='F') tr td ◯ td From 6a510a389d97432f36fde796b15204e1796bedaa Mon Sep 17 00:00:00 2001 From: jssunray34 <55996087+jssunray34@users.noreply.github.com> Date: Sun, 26 Mar 2023 21:09:20 -0400 Subject: [PATCH 02/54] Validate tautology --- src/common/statement.ts | 166 ++++++++++++++++++++++++++++++++++++++++ src/common/tree.ts | 14 ++++ 2 files changed, 180 insertions(+) diff --git a/src/common/statement.ts b/src/common/statement.ts index 46bf53b..9158f0d 100644 --- a/src/common/statement.ts +++ b/src/common/statement.ts @@ -14,6 +14,22 @@ export abstract class Statement { ); } + isTautology(): boolean { + if (this instanceof OrStatement) { + const lhs = this.operands[0]; + const rhs = this.operands[1]; + console.log("lhs: " + lhs); + console.log("rhs: " + rhs); + if (lhs.equals(new NotStatement(rhs))) { + return true; + } else if (rhs.equals(new NotStatement(lhs))) { + return true; + } + } + + return false; + } + /** * Decomposes this statement into an array of branches, where each branch * contains the necessary decomposed statements. @@ -583,3 +599,153 @@ class StatementEquivalenceEvaluator { return false; } } + +export class StatementReducer { + statement: Statement; + + constructor(statement: Statement) { + this.statement = statement; + } + + /** + * Checks if the conclusion is a valid not reduction of this statement + * given the literal. + * @param literal the branch taken (e.g., H or ¬H) + * @param conclusion the predicted conclusion + */ + private checkNotReduction(assertion: Statement, conclusion: Statement): boolean { + if (this.statement instanceof NotStatement) { + console.log("NotStatment!") + console.log(this.statement.operand); + let operand = this.statement.operand; + if (assertion.equals(operand)) { + return conclusion instanceof Contradiction; + } else if (assertion.equals(new NotStatement(operand))) { + return conclusion instanceof Tautology; + } + } + + return false; + } + + /** + * Checks if the conclusion is a valid and reduction of this statement + * given the literal. + * @param literal the branch taken (e.g., H or ¬H) + * @param conclusion the predicted conclusion + */ + private checkAndReduction(assertion: Statement, conclusion: Statement): boolean { + if (this.statement instanceof AndStatement) { + console.log("AndStatement!"); + console.log("left: " + this.statement.operands[0]); + console.log("right: " + this.statement.operands[1]); + let lhs = this.statement.operands[0]; + let rhs = this.statement.operands[1]; + if (assertion.equals(lhs)) { + return conclusion.equals(rhs); + } else if (assertion.equals(rhs)) { + return conclusion.equals(lhs); + } else if (assertion.equals(new NotStatement(lhs))) { + return conclusion instanceof Contradiction; + } else if (assertion.equals(new NotStatement(rhs))) { + return conclusion instanceof Contradiction; + } + } + + return false; + } + + /** + * Checks if the conclusion is a valid or reduction of this statement + * given the literal. + * @param literal the branch taken (e.g., H or ¬H) + * @param conclusion the predicted conclusion + */ + private checkOrReduction(assertion: Statement, conclusion: Statement): boolean { + if (this.statement instanceof OrStatement) { + console.log("OrStatement!"); + console.log("left: " + this.statement.operands[0]); + console.log("right: " + this.statement.operands[1]); + let lhs = this.statement.operands[0]; + let rhs = this.statement.operands[1]; + if (assertion.equals(lhs)) { + return conclusion instanceof Tautology; + } else if (assertion.equals(rhs)) { + return conclusion instanceof Tautology; + } else if (assertion.equals(new NotStatement(lhs))) { + return conclusion.equals(rhs); + } else if (assertion.equals(new NotStatement(rhs))) { + return conclusion.equals(lhs); + } + } + + return false; + } + + /** + * Checks if the conclusion is a valid conditional reduction of this statement + * given the literal. + * @param literal the branch taken (e.g., H or ¬H) + * @param conclusion the predicted conclusion + */ + private checkConditionalReduction(assertion: Statement, conclusion: Statement): boolean { + if (this.statement instanceof ConditionalStatement) { + console.log("ConditionalStatement!"); + console.log("left: " + this.statement.lhs); + console.log("right: " + this.statement.rhs); + let lhs = this.statement.lhs; + let rhs = this.statement.rhs; + if (assertion.equals(lhs)) { + return conclusion.equals(rhs); + } else if (assertion.equals(rhs)) { + return conclusion instanceof Tautology; + } else if (assertion.equals(new NotStatement(lhs))) { + return conclusion instanceof Tautology; + } else if (assertion.equals(new NotStatement(rhs))) { + return conclusion.equals(new NotStatement(lhs)); + } + } + + return false; + } + + /** + * Checks if the conclusion is a valid biconditional reduction of this statement + * given the literal. + * @param literal the branch taken (e.g., H or ¬H) + * @param conclusion the predicted conclusion + */ + private checkBiconditionalReduction(assertion: Statement, conclusion: Statement): boolean { + if (this.statement instanceof BiconditionalStatement) { + console.log("BiconditionalStatement!"); + console.log("left: " + this.statement.lhs); + console.log("right: " + this.statement.rhs); + let lhs = this.statement.lhs; + let rhs = this.statement.rhs; + if (assertion.equals(lhs)) { + return conclusion.equals(rhs); + } else if (assertion.equals(rhs)) { + return conclusion.equals(lhs); + } else if (assertion.equals(new NotStatement(lhs))) { + return conclusion.equals(new NotStatement(rhs)); + } else if (assertion.equals(new NotStatement(rhs))) { + return conclusion.equals(new NotStatement(lhs)); + } + } + + return false; + } + + /** + * Verifies whether the conclusion is a valid reduction (i.e., it must satisfy + * one of the reduction rules). + * @returns true if the conclusion is valid and false otherwise + */ + validateReduction(assertion: Statement, conclusion: Statement): boolean { + return this.checkNotReduction(assertion, conclusion) || + this.checkAndReduction(assertion, conclusion) || + this.checkOrReduction(assertion, conclusion) || + this.checkConditionalReduction(assertion, conclusion) || + this.checkBiconditionalReduction(assertion, conclusion); + } +} diff --git a/src/common/tree.ts b/src/common/tree.ts index 227f274..e61b799 100644 --- a/src/common/tree.ts +++ b/src/common/tree.ts @@ -107,6 +107,7 @@ export class TruthTreeNode { private _text = ''; private _statement: Statement | null = null; premise = false; + isTautology = false; comment: string | null = null; tree: TruthTree; @@ -139,6 +140,7 @@ export class TruthTreeNode { const newNode = new TruthTreeNode(this.id, newTree); newNode.text = this.text; newNode.premise = this.premise; + newNode.isTautology = this.isTautology; newNode.comment = this.comment; newNode.parent = this.parent; newNode.children = [...this.children]; @@ -238,6 +240,9 @@ export class TruthTreeNode { */ set statement(newStatement: Statement | null) { this._statement = newStatement; + if (this._statement?.isTautology()) { + this.isTautology = true; + } this._correctDecomposition = null; // Anything that references this is also invalid. if (this.antecedent !== null) { @@ -589,6 +594,11 @@ export class TruthTreeNode { return true; } + if (this.isTautology) { + // Tautologies are always valid + return true; + } + // Non-premises must have an antecedent for this statement to be valid if (this.antecedent === null || !(this.antecedent in this.tree.nodes)) { return new CorrectnessError('not_logical_consequence'); @@ -939,6 +949,10 @@ export class TruthTreeNode { return 'This statement is a premise.'; } + if (this.isTautology) { + return 'This statement is a tautology.'; + } + if (this.isTerminator()) { if (this.isOpenTerminator()) { return 'This open branch represents a valid assignment.'; From aca67bc4bc578504fa1779064c0ae2c64d573e37 Mon Sep 17 00:00:00 2001 From: jssunray34 <55996087+jssunray34@users.noreply.github.com> Date: Sun, 2 Apr 2023 13:05:57 -0400 Subject: [PATCH 03/54] Create new modifyDecomposition and add call to validateReduction Co-Authored-By: Jenny Gao <29582421+jeninyg@users.noreply.github.com> --- src/client/component/truth-tree-branch.ts | 31 ++++++++++++++++++++++- src/common/tree.ts | 14 ++++++++++ 2 files changed, 44 insertions(+), 1 deletion(-) diff --git a/src/client/component/truth-tree-branch.ts b/src/client/component/truth-tree-branch.ts index d00394e..9db27c6 100644 --- a/src/client/component/truth-tree-branch.ts +++ b/src/client/component/truth-tree-branch.ts @@ -76,6 +76,27 @@ export const TruthTreeBranchComponent = defineComponent({ this.childBranches.push(ref); } }, + modifyDecompositionDP(id: number) { + // TODO: Document this function more + const selectedNode: TruthTreeNode | null = + this.$store.getters.selectedNode; + + if (selectedNode === null || selectedNode.id === id) { + return; + } + + if (selectedNode.decomposition.has(id)) { + selectedNode.decomposition.delete(id); + } else { + selectedNode.decomposition.add(id); + } + const decomp = Array.from(selectedNode.decomposition); + for (let i = 0; i < decomp.length; i++) { + // console.log("hello"); + // console.log(decomp[i]); + console.log(this.tree.nodes[decomp[i]]); + } + }, /** * Adds or removes a given node from the decomposition of the selected node, * or vice-versa depending on the position of the selected node relative to @@ -101,6 +122,14 @@ export const TruthTreeBranchComponent = defineComponent({ } else { selectedNode.decomposition.add(id); } + const decomp = Array.from(selectedNode.decomposition); + for (let i = 0; i < decomp.length; i++) { + // console.log("hello"); + // console.log(decomp[i]); + console.log(this.tree.nodes[decomp[i]]); + } + // let first = decomp[0] + // console.log(this.tree.nodes[decomp[0]]) } else if (selectedNode.isAncestorOf(id)) { // When the selected is BEFORE, it becomes decomposition const otherNode: TruthTreeNode = this.$store.state.tree.nodes[id]; @@ -211,7 +240,7 @@ export const TruthTreeBranchComponent = defineComponent({