Questions tagged [propositional-logic]

The tag has no usage guidance.

31 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
4
votes
0answers
45 views

Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
3
votes
3answers
559 views

Does exist any horn formula that is equisatisfiable to the clause that is disjunction of two literals? Does also exist equivalent?

I just and simply want to know if whether or not exist any horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to know if there also exists equivalent.
2
votes
0answers
47 views

An optimization version of 2QBF: is it $\mathsf{NP}^{\mathsf{NP}}$-hard?

I am studying the computational complexity of the following decision problem related to 2QBF: Input: a 3-CNF formula $\varphi$ over $X \cup Y$, where $X$, $Y$ are disjoint sets of propositional ...
2
votes
0answers
43 views

Large Conjunctive Normal Form Examples

I'm currently learning about conjunctive normal form in a course on logic for Computer Science. I was reading the Wikipedia entry on the subject and encountered this: Typical problems in this case ...
2
votes
0answers
97 views

A Quine–McCluskey variant for conjunctive normal formal?

There is the Quine–McCluskey algorithm for finding a minimal expression of a boolean expression in dis-junctive normal form. Would applying DeMorgan's rule to the minimal DNF result in the minimal CNF?...
2
votes
0answers
93 views

Why Modus ponens works with Horn clauses and Generalized Modus ponens requires definite clauses?

I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward ...
2
votes
0answers
61 views

What is the difference between the situation calculus and the propositional logic of context?

I have been reading a lot of papers by John McCarthy lately. As early as 1963, he developed the situation calculus, but then starting in 1987, he developed what came to be known as the propositional ...
1
vote
1answer
32 views

Proving the validity of a sequent using Modus Tollens

Problem: Prove $p \rightarrow (q \vee r), \neg q, \neg r \vdash \neg p$ using Modus Tollens. I need to prove the validity of the above sequent by using natural deduction. Initially, I didn't read the ...
1
vote
0answers
20 views

Computational complexity in Boolean network

An Boolean control networks can be expressed as \begin{equation} \label{ControlBN} \left\{\begin{array}{l}{x_{1}(t+1)=f_{1}\left(x_{1}(t), \cdots, x_{n}(t), u_{1}(t), \cdots, u_{m}(t)\right),} \\ {x_{...
1
vote
0answers
24 views

Correctness of Simple Programs

For a homework assignment I am asked to provide claim sequences to verify that the given conditional does indeed satisfy its specification (to compute in r the absolute value of x). ...
1
vote
0answers
99 views

How to minimize large DNF formula into deeper but smaller formula?

I want to minimize DNF formula which has ~200k products combined into a sum. The depth of that formula is 2 - first level is the OR, and second level is AND for all conjunctions. I have tried using ...
1
vote
0answers
69 views

What is the definition of the property of Canonicity for a logic?

I'm trying to understand "A Systematic Approach to Canonicity in the Classical Sequent Calculus" by Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. The article discusses a property called "canonicity" ...
1
vote
0answers
72 views

Refutation of pigeonhole using resolution

I am trying to find a way to refute the pigeonhole formula using resolution. Lets assume that $x_{ij}$ is true if $i^{th}$ pigeon is in $j^{th}$ hole. Thus, with $n$ holes and $n+1$ pigeons, the ...
1
vote
0answers
264 views

Propositional logic in an SMA* algorithm

I'm trying to implement an SMA* graph search algorithm that I found in a paper here(Rong Zhou, Eric A. Hansen: Memory-Bounded A* Graph Search. FLAIRS-02 Proceedings 203-209) and I would like to ...
1
vote
0answers
35 views

What does the structure ($S_t^x P$) in this Existantial Instantiation imply, Skolemization?

The sheet of equivalences given to us in class provides the two equivalences \begin{array}{|c|c|c|} \hline \text{Universal Instantiation} & \forall x ~ P(x) \implies {S_t}^x P & \exists y ~ \...
1
vote
0answers
80 views

Efficiently decidable logics

So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then ...
0
votes
1answer
28 views

Is Conjunctive Normal Form or not?

I have one formula that I do not understand why it is CNF and one that is not CNF, namely. p && !q (NOT NCF) and !!p(CNF). According to the exercise where I found these examples, 1 is not ...
0
votes
0answers
43 views

When are existential quantifiers in the intuitionistic propositional calculus eliminable and when not

I am so ignorant I don't even know where should I ask this - on FOM? On mathoverflow? On cstheory? So please consider as sort of a meta-question readdressing me in case you think this is a wrong site. ...
0
votes
0answers
14 views

Satisfaction of CTL

I'm trying to compute Sat(Φ), but I can't seem to figure out this question, what i understood is that I first need to solve Sat(req U -busy), but it doesn't make sense, how can it be that req is true ...
0
votes
0answers
31 views

Simplify logical expression represented as binary tree

I implemented logical expressions using a binary tree in C++. Now I want to be able to simplify such an expression using rules like e.g. but have issues with the commutativity. Assuming the ...
0
votes
1answer
50 views

What does it mean to “show algebraically” in propositional logic?

The biconditional operator $\iff$ of Propositional Logic can be defined by the identity $p \iff q \equiv (\lnot p \lor q) \land (\lnot q \lor p) \quad (1.1)$ Use the identity $(1.1)$ and identities ...
0
votes
0answers
25 views

About the complexity of deciding if the closed world assumption for renamable Horn CNF is consistent

Let $T$ be a theory that only contains renamable horn formulas. What is the complexity of deciding if the closed world assumption $CWA(T)$ is consistent? The closed world assumption is defined as ...
0
votes
1answer
40 views

Consistent theory based on L and not(A->A) is a theorem

I am working on this problem in which I have a theory $T$ based on language $\mathcal{L}$ and the only information we have is that T is consistent and $\vdash \lnot(A \rightarrow A)$. Given this ...
0
votes
0answers
40 views

How to write negation of an 'AND' statement in logic

Suppose the given proposition is: "Zach blocks emails and texts from Jennifer" Where, P implies "Zach blocks emails from Jennifer". Q implies "Zach blocks texts from Jennifer". So it's P AND Q in ...
0
votes
0answers
57 views

What are necessity and sufficiency?

I was reading deadlock topic from Operating Systems book by Stallings. It states four pre requisites for deadlock: Mutual exclusion No preemption Hold and wait Circular wait It then have following ...
0
votes
1answer
129 views

How to construct an NFA Ai for the given Regular property P1 and P2?

Let AP = {a; b; c}. Consider the following regular safety properties: (a) P1: If a becomes valid, afterwards b stays valid ad infinitum or until c holds. (b) P2: Between two neighbouring occurrences ...
0
votes
0answers
51 views

Resolution with multiple variables

Resolution allows to generate new clauses for an existing set of clauses. In many cases, the rule is simple: ...
0
votes
0answers
114 views

Convert conjunctive normal form to equivalent boolean formula with only NOR gates

Let $\varphi$ be a boolean formula in 3-CNF form (conjunctive normal form with three literals at most per clause). I want to convert it to an equivalent boolean formula that uses only NOR gates with ...
-1
votes
0answers
19 views

Writing an equivalent to (p->q)/\r using only ∼ and ∨

Trying to write (p->q)/\r using only ∼ and ∨ but always getting stuck .
-1
votes
3answers
81 views

Prove (p → ¬q) is equivalent to ¬(p ∧ q)

I need to prove the above sequent using natural deduction. I did the first half already i.e. I proved $(p\rightarrow\neg q)\rightarrow \neg (p \wedge q)$, but I'm stuck on where to start for the ...
-1
votes
1answer
24 views

C logical consequence of S iff S union {-C} UNSAT

I'm trying to do the following demonstration: (C and S are CNF) C is a logical consequence of S iff. S u {-C} UNSAT And I did the following: C is a logical consequence of S iff. S u {-C} UNSAT iff. ...