Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
125
questions
0
votes
0answers
40 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 ...
1
vote
1answer
15 views
Context-free grammar for tautologies in one variable
Construct a context-free grammar for the set of tautologies in $p$ - that is, the set of formulae in $\{p, \text{true}, \text{false}, \land, \lor, \lnot, (, )\}$ which evaluate to $\text{true}$ for ...
1
vote
2answers
84 views
Are $\mathsf{\#P}$ problems harder than $\mathsf{NP}$ problems
I have a method to solve the $\mathsf{\#P}$ version of 3SAT in a way that seemingly reduces it to an $\mathsf{NP}$ problem. - I don't have a formal understanding of these terms so I will just show an ...
2
votes
1answer
61 views
3-CNF to “independent form”
Is it possible to convert all logical formulae into a form such that each variable ends up in exactly 1 "factor" of the and operation? ($\wedge$). Any combination of operations is allowed, though the ...
2
votes
1answer
42 views
Conjunctive normal form to simple elementary algebra
I'm curious to know the computational complexity class of each step in this method of converting a CNF formula into simple elementary algebra.
An example:
$$\phi=\left(x_1 \vee x_2 \right) \wedge \...
0
votes
1answer
27 views
Algorithm for automatic construction of natural deduction proofs
I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic.
If there is no algoritm, can you ...
2
votes
0answers
23 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?...
4
votes
3answers
97 views
Is it a tautology or not? According to my truth table its not
If $\bigr((q\leftrightarrow p)\leftrightarrow s\bigl)$ is a tautology and $p\rightarrow s$ is contingent, does it follow that $q\rightarrow s$ is contingent?
Since I can't show $\bigr((q\...
3
votes
0answers
31 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 ...
2
votes
1answer
24 views
How do I determine if this argument is valid?
I'm studying propositional logic the section on "valid arguments".
A self-assessment question reads
"Show whether or not the following argument is valid"
$\frac{P}{C}$
I don't know what function ...
1
vote
1answer
24 views
Does “$\forall x\in L, \sigma(\neg x)=\neg \sigma(x)$” hold given that $\sigma(F)\equiv F$ for a CNF formula $F$ built on a set $L$ of literals?
Suppose we have a CNF formula $F$ built on the set of literals $L=\{x_1,\neg x_1,\cdots,x_n,\neg x_n\}$ where each variable is used in at least one clause of $F$. Consider a permutation $\sigma$ of $L$...
0
votes
2answers
40 views
Why we treat sentence letter $Q$ as conclusion in one form and premise in other?
Sorry for asking such a dumb question.
I am CS student and I am trying to understand the basic tenets of Logic. I am new to the subject and I am lost understanding Implication.
In formal logic, $(P\...
3
votes
1answer
68 views
Matrix Representation for logical gates?
I have been trying to find if there are other matrix type representations logical circuits, in the example below, $$\begin{bmatrix} 1 & 0\\ 1 & 1\\ \end{bmatrix} \equiv \, \, \Rightarrow$$ ...
2
votes
0answers
40 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 ...
0
votes
1answer
144 views
Can this set of propositions be represented and proved in Haskell?
I used a set of natural language statements and their formalization from Gries and Schneider. I attempted to transform the propositions into Haskell equations. For example, for S0 : $a \land w \...
1
vote
1answer
53 views
What is the computational complexity of intuitionistic propositional logic?
Consider the decision problem: given formulas of propositional logic $\phi_1, \ldots, \phi_n, \psi$, determine whether $\phi_1, \ldots, \phi_n \vdash \psi$ intuitionistically. This problem is well-...
0
votes
1answer
41 views
Finding CNF of $(p \rightarrow q) \rightarrow p$ and $\lnot (q \wedge (\lnot p \rightarrow q)) $
I'm trying to find the CNF of the $(p \rightarrow q) \rightarrow p$ and $\lnot (q \wedge (\lnot p \rightarrow q))$, and afterwards proving it's validity. As i'm new to CNF i wanted to ensure i've ...
2
votes
0answers
24 views
Is there a formula that is not logical equivalent to any Horn clause?
There are of course formulas that can't be transformed into a Horn clause but is it possible to construct an equivalent Horn clause that is true under the same interpretation?
1
vote
0answers
45 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
votes
1answer
22 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.
...
2
votes
1answer
44 views
Does it hold that $F \equiv \sigma(F)$ for a CNF formula $F$ and a permutation $\sigma$ s.t. $F \vDash \sigma(F)$?
Suppose we have a CNF formula $F$ and a permutation $\sigma$ of its literals such that for any literal $x, \sigma(\neg x)=\neg \sigma(x)$ and $F \vDash \sigma(F)$.
Does it hold that $F \equiv \sigma(...
4
votes
1answer
121 views
Knight and knaves
I have these in my lecture notes, its about the rules where knights always tell the truth and knaves always lie:
If A says “The statement ‘there is gold on the island’ and the statement ‘I am a ...
2
votes
1answer
36 views
Preserving a propositional formula
I know I must be getting stuck on notation. However, I'm having trouble following the logic in Example 1.2 in https://arxiv.org/pdf/cs/0611018.pdf. They define what preserving a propositional ...
1
vote
1answer
131 views
How to define the Atomic Propositions in Model Checking
The atomic propositions in Symbolic Model Checking form the state in the state-transition graph (the model $\mathcal{M}$ in Model Checking). The other part of Model Checking is the specification, ...
2
votes
1answer
62 views
Are there any techniques for checking whether a clause is subsumed by another clause when adding it to a cnf formula?
When doing variable elimination on a formula in cnf form, there is created a lot of new clauses. Is there any efficient way to check if these are subsumed by other, already existing clauses?
1
vote
1answer
112 views
Resolution Algorithm - No new clauses
The standard resolution algorithm returns false if no new clauses are added.
I know that if $KB \land \neg a \implies []$, it returns true by proof by contradiction, but how can I understand the ...
3
votes
1answer
121 views
What is the connection between combinatorial circuits and finite state automata?
The diagram on the Wikipedia page of FSA shows the hierarchy of the computational devices, in that diagram it is denoted that the finite state machines are superior to the combinatorial circuits.
...
0
votes
2answers
71 views
Can any memory-less computer operation be represented in propositional logic?
Take any operation that is done by any type of computer (e.g. a cpu on a modern laptop), which doesn't use any type of temporary memory storage.
I.e. this computer operation computes a function $f(x)=...
0
votes
0answers
36 views
Give context-free grammars that generate formulas in: [duplicate]
Give context-free grammars that generate formulas in propositional calculus, taking into account:
variables represented by single lowercase letter
Operations are conjunction (∧), disjunction (∨), ...
0
votes
1answer
34 views
Convert (x + y = z) to propositional logic formula for 8-bit numbers
(Note: this was asked in the cstheory stackexchange, but I was told this is a more appropriate place for it.)
I have three 8-bit 2's-complement numbers (X, Y, and Z). I want to find a propositional ...
1
vote
0answers
66 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" ...
0
votes
1answer
61 views
Inference rules for deriving invariants in Hoare logic
The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string):
...
0
votes
0answers
76 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 ...
18
votes
4answers
5k views
Can proof by contradiction work without the law of excluded middle?
I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
12
votes
5answers
2k views
Why does soundness imply consistency?
I was reading the question Consistency and completeness imply soundness? and the first statement in it says:
I understand that soundness implies consistency.
Which I was quite puzzled about ...
5
votes
1answer
300 views
Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence
I have to ask for forgiveness in advance if the whole question doesn't
make a lot of sense, but unfortunately, I have no better intuition as
of right now and this seems like the best starting point I ...
1
vote
2answers
765 views
how to solve Hoare logic problems
I'm having trouble proving Hoare logic questions as I'm not sure of the process that is taken to prove them. I understand that they're rules such as assignment axiom, pre-condition strengthening, post-...
0
votes
1answer
72 views
Does exist NP language that is Cook Levin deterministic reducible to xor satisfiability in polynomial time?
We say that the language $L$ is Cook Levin deterministic reducible to xor satisfiability in polynomial time if and only if for each word $w\in\Sigma^*:w\in L\iff f(w)\in XORSAT$ where $\Sigma=\{0,1\}$ ...
0
votes
1answer
131 views
Is this possible to solve satisfiability by using Quine McCluskey algorithm to simplify the whole given boolean formula by simplifying subformulas?
In this question
Farewell Stack Exchange suggested to use karnaugh maps to solve the satisfiability problem by simplifying the entire/whole boolean formula by simplifying subformulas until you have ...
0
votes
2answers
4k views
Which of the following expressions is TRUE if and only if NOT all three variables a, b, and c have the same value?
I am trying to solve this problem and I am stuck. I think it is B, but I think I'm wrong. Thanks.
Which of the following expressions is TRUE if and only if NOT all three variables a, b, and c have ...
3
votes
3answers
304 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.
3
votes
1answer
265 views
How to estimate how many assignments satisfy a given DNF formula using Monte Carlo?
Admittedly, homework.
For the purpose of this question: $\phi$ is a DNF formula similar to this one: $(x_1 \wedge \neg x_3 \wedge x_4) \vee (\neg x_1 \wedge x_2)$ Also $C_i$ is a clause in this ...
3
votes
2answers
79 views
Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?
Recently I was reading again this propositions as types paper by Philip Wadler:
http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
It gives an impression, ...
1
vote
1answer
87 views
How to adapt DPLL to solve HORNSAT?
This question wask asked in a homework of Computer Theory in Rome, Italy.
How to simplify the DPLL algorithm in order to solve HORNSAT?
My Approach:
I know that an Horn clause is an OR of ...
21
votes
11answers
4k views
Why is $A \lor (A \land \neg B) \equiv A$?
I would like to know if there is a rule to prove this. For example, if I use the distributive law I will get only $(A \lor A) \land (A \lor \neg B)$.
-4
votes
1answer
115 views
Valid, unsatisfied or neither? [closed]
How should I create the truth table to solve each of these questions? Maybe can give me an example?
$Smoke \implies Smoke$
$Smoke \implies Fire$
$(Smoke \implies Fire) \implies (\neg Smoke \implies \...
1
vote
3answers
57 views
Expressing statements on elephants in propositional logic
If I wanted to create a sentence like:
African elephants can carry coconuts; Asian elephants cannot.
How would I do that with propositional logic?
2
votes
4answers
235 views
Is it necessary to learn how to prove Mathematical theorems as a CS Student? [closed]
I've just started my undergraduate course and have tried my hands on MIT's OpenCourseWare on Discrete Math on Logic and Proofs. There was a particular question asking to prove Cantor's Theorem:
...
1
vote
1answer
324 views
Question on Predicates and Quantifiers
I am reading from "Discrete Mathematics and Its applications" by Kenneth H. Rosen, 7th edition. Consider the highlighted part in the following example taken from the same book:
Question Use ...
1
vote
1answer
222 views
cancel out parts of a formula in CNF (conjunctive normal form)
In this image there is a given formula in DNF and CNF. When I check it on Wolfram Alpha I see that it cancel out (E or D) because of (not A or A) which is colored in red. My question is if it is ...
