Dtjytyk

Do I have to take mana from my deck or hand when tapping this card?

Travelling in US for more than 90 days

Air travel with refrigerated insulin

Is this Pascal's Matrix?

Relations between homogeneous polynomials

Has the laser at Magurele, Romania reached a tenth of the Sun's power?

What is the meaning of "You've never met a graph you didn't like?"

Walter Rudin's mathematical analysis: theorem 2.43. Why proof can't work under the perfect set is uncountable.

How to preserve electronics (computers, ipads, phones) for hundreds of years?

Would a primitive species be able to learn English from reading books alone?

What is the purpose of using a decision tree?

Highest stage count that are used one right after the other?

What is the tangent at a sharp point on a curve?

Would this string work as string?

Sort with assumptions

Why can't I get pgrep output right to variable on bash script?

Is this saw blade faulty?

Can you describe someone as luxurious? As in someone who likes luxurious things?

Why do Radio Buttons not fill the entire outer circle?

Why is implicit conversion not ambiguous for non-primitive types?

What properties make a magic weapon befit a Rogue more than a DEX-based Fighter?

What is it called when someone votes for an option that's not their first choice?

What should be the ideal length of sentences in a blog post for ease of reading?

How do I lift the insulation blower into the attic?

SAT for a formula using Tableaux Propositional Logic (precedence of operators)

Need help with solving proposition logic formula, should be a tautologyPropositional logic and distributive lawHelp with natural deduction (Propositional logic)Motivation for signed tableaux rules for propositional intuitionistic logiclogic: derive a formula using lawsclause “elimination” using assumptions in a propositional formulaHow to prove this propositional logic equation?Initialization in the tableaux method for first order logicPropositional logic proof checkGiven is a set of clauses. Find a logic formula in CNF such that..

1

$begingroup$

My doubt is in check if the following formula $phi$ is SAT or not using the Tableaux Method. Let me write formula:

$phi = neg left ( p vee q supset left ( left ( neg p wedge q right ) vee p vee neg q right ) right )$

How start rules of tableaux method in this case?

logic propositional-calculus formal-languages satisfiability

share|cite|improve this question

edited Mar 12 at 21:02

mayday24

asked Mar 12 at 15:35

mayday24mayday24

83

$endgroup$

add a comment | 

1

$begingroup$

My doubt is in check if the following formula $phi$ is SAT or not using the Tableaux Method. Let me write formula:

$phi = neg left ( p vee q supset left ( left ( neg p wedge q right ) vee p vee neg q right ) right )$

How start rules of tableaux method in this case?

logic propositional-calculus formal-languages satisfiability

share|cite|improve this question

edited Mar 12 at 21:02

mayday24

asked Mar 12 at 15:35

mayday24mayday24

83

$endgroup$

add a comment | 

$begingroup$

My doubt is in check if the following formula $phi$ is SAT or not using the Tableaux Method. Let me write formula:

$phi = neg left ( p vee q supset left ( left ( neg p wedge q right ) vee p vee neg q right ) right )$

How start rules of tableaux method in this case?

logic propositional-calculus formal-languages satisfiability

share|cite|improve this question

edited Mar 12 at 21:02

mayday24

asked Mar 12 at 15:35

mayday24mayday24

83

$endgroup$

share|cite|improve this question

edited Mar 12 at 21:02

mayday24

asked Mar 12 at 15:35

mayday24mayday24

83

share|cite|improve this question

edited Mar 12 at 21:02

mayday24

asked Mar 12 at 15:35

mayday24mayday24

83

asked Mar 12 at 15:35

mayday24mayday24

83

asked Mar 12 at 15:35

mayday24mayday24

83

2 Answers
2

active

oldest

votes

0

$begingroup$

You have to apply the rule corresponding to the principal connective of the negated formula.

Assuming the usual convention for omitting parentheses, we have that conjunction and disjunction symbols apply to as little as possible.

Thus, the formula will be read as :

$¬[(p∨q) to ((¬p∧q)∨p∨¬q)]$.

In this case, the formula is the negation of a conditional; thus, you have to start using the rule :

$lnot (alpha to beta)$.

share|cite|improve this answer

edited Mar 12 at 15:45

answered Mar 12 at 15:39

Mauro ALLEGRANZAMauro ALLEGRANZA

67.2k449115

$endgroup$

add a comment | 

0

$begingroup$

Thank you! I apply the rest of Tableaux Method if can be useful for someone.

$p vee q$ $[mu_1]$from rule of AND. I apply tableaux method for this point later..

$ neg ( (neg p wedge q) vee p vee neg q)$ from rule of AND, associative property

$ neg (neg p wedge q) wedge neg(p vee neg q)$ de Morgan property

$neg (neg p wedge q) $ rule of AND

$neg(p vee neg q)$ rule of OR

$p vee neg q $ $[mu_2]$

$neg p wedge q $

$neg p$

$q$

..apply first OR $[mu_1]$

$beta_1$ branch: $p$ clash! Branch closed.

$beta_2$ branch: $q$

..apply second OR $[mu_2]$

$beta_{2_1}$ branch: $p$ clash! Branch closed.

$beta_{2_2}$ branch: $neg q$ clash! Branch closed.

We can say that $phi$ is UNSAT.

share|cite|improve this answer

edited Mar 12 at 16:20

answered Mar 12 at 16:15

mayday24mayday24

83

$endgroup$

add a comment | 

Your Answer

StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");

StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});

function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});


}
});

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name

Email

Required, but never shown

StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3145230%2fsat-for-a-formula-using-tableaux-propositional-logic-precedence-of-operators%23new-answer', 'question_page');
}
);

Post as a guest

Name

Email

Required, but never shown

0

$begingroup$

You have to apply the rule corresponding to the principal connective of the negated formula.

Assuming the usual convention for omitting parentheses, we have that conjunction and disjunction symbols apply to as little as possible.

Thus, the formula will be read as :

$¬[(p∨q) to ((¬p∧q)∨p∨¬q)]$.

In this case, the formula is the negation of a conditional; thus, you have to start using the rule :

$lnot (alpha to beta)$.

share|cite|improve this answer

edited Mar 12 at 15:45

answered Mar 12 at 15:39

Mauro ALLEGRANZAMauro ALLEGRANZA

67.2k449115

$endgroup$

add a comment | 

0

$begingroup$

You have to apply the rule corresponding to the principal connective of the negated formula.

Assuming the usual convention for omitting parentheses, we have that conjunction and disjunction symbols apply to as little as possible.

Thus, the formula will be read as :

$¬[(p∨q) to ((¬p∧q)∨p∨¬q)]$.

In this case, the formula is the negation of a conditional; thus, you have to start using the rule :

$lnot (alpha to beta)$.

share|cite|improve this answer

edited Mar 12 at 15:45

answered Mar 12 at 15:39

Mauro ALLEGRANZAMauro ALLEGRANZA

67.2k449115

$endgroup$

add a comment | 

$begingroup$

You have to apply the rule corresponding to the principal connective of the negated formula.

Assuming the usual convention for omitting parentheses, we have that conjunction and disjunction symbols apply to as little as possible.

Thus, the formula will be read as :

$¬[(p∨q) to ((¬p∧q)∨p∨¬q)]$.

In this case, the formula is the negation of a conditional; thus, you have to start using the rule :

$lnot (alpha to beta)$.

share|cite|improve this answer

edited Mar 12 at 15:45

answered Mar 12 at 15:39

Mauro ALLEGRANZAMauro ALLEGRANZA

67.2k449115

$endgroup$

share|cite|improve this answer

edited Mar 12 at 15:45

answered Mar 12 at 15:39

Mauro ALLEGRANZAMauro ALLEGRANZA

67.2k449115

answered Mar 12 at 15:39

Mauro ALLEGRANZAMauro ALLEGRANZA

67.2k449115

answered Mar 12 at 15:39

Mauro ALLEGRANZAMauro ALLEGRANZA

67.2k449115

0

$begingroup$

Thank you! I apply the rest of Tableaux Method if can be useful for someone.

$p vee q$ $[mu_1]$from rule of AND. I apply tableaux method for this point later..

$ neg ( (neg p wedge q) vee p vee neg q)$ from rule of AND, associative property

$ neg (neg p wedge q) wedge neg(p vee neg q)$ de Morgan property

$neg (neg p wedge q) $ rule of AND

$neg(p vee neg q)$ rule of OR

$p vee neg q $ $[mu_2]$

$neg p wedge q $

$neg p$

$q$

..apply first OR $[mu_1]$

$beta_1$ branch: $p$ clash! Branch closed.

$beta_2$ branch: $q$

..apply second OR $[mu_2]$

$beta_{2_1}$ branch: $p$ clash! Branch closed.

$beta_{2_2}$ branch: $neg q$ clash! Branch closed.

We can say that $phi$ is UNSAT.

share|cite|improve this answer

edited Mar 12 at 16:20

answered Mar 12 at 16:15

mayday24mayday24

83

$endgroup$

add a comment | 

0

$begingroup$

Thank you! I apply the rest of Tableaux Method if can be useful for someone.

$p vee q$ $[mu_1]$from rule of AND. I apply tableaux method for this point later..

$ neg ( (neg p wedge q) vee p vee neg q)$ from rule of AND, associative property

$ neg (neg p wedge q) wedge neg(p vee neg q)$ de Morgan property

$neg (neg p wedge q) $ rule of AND

$neg(p vee neg q)$ rule of OR

$p vee neg q $ $[mu_2]$

$neg p wedge q $

$neg p$

$q$

..apply first OR $[mu_1]$

$beta_1$ branch: $p$ clash! Branch closed.

$beta_2$ branch: $q$

..apply second OR $[mu_2]$

$beta_{2_1}$ branch: $p$ clash! Branch closed.

$beta_{2_2}$ branch: $neg q$ clash! Branch closed.

We can say that $phi$ is UNSAT.

share|cite|improve this answer

edited Mar 12 at 16:20

answered Mar 12 at 16:15

mayday24mayday24

83

$endgroup$

add a comment | 

$begingroup$

Thank you! I apply the rest of Tableaux Method if can be useful for someone.

$p vee q$ $[mu_1]$from rule of AND. I apply tableaux method for this point later..

$ neg ( (neg p wedge q) vee p vee neg q)$ from rule of AND, associative property

$ neg (neg p wedge q) wedge neg(p vee neg q)$ de Morgan property

$neg (neg p wedge q) $ rule of AND

$neg(p vee neg q)$ rule of OR

$p vee neg q $ $[mu_2]$

$neg p wedge q $

$neg p$

$q$

..apply first OR $[mu_1]$

$beta_1$ branch: $p$ clash! Branch closed.

$beta_2$ branch: $q$

..apply second OR $[mu_2]$

$beta_{2_1}$ branch: $p$ clash! Branch closed.

$beta_{2_2}$ branch: $neg q$ clash! Branch closed.

We can say that $phi$ is UNSAT.

share|cite|improve this answer

edited Mar 12 at 16:20

answered Mar 12 at 16:15

mayday24mayday24

83

$endgroup$

share|cite|improve this answer

edited Mar 12 at 16:20

answered Mar 12 at 16:15

mayday24mayday24

83

answered Mar 12 at 16:15

mayday24mayday24

83

answered Mar 12 at 16:15

mayday24mayday24

83