Questions tagged [propositional-logic]
The propositional-logic tag has no usage guidance.
142
questions
2
votes
1answer
20 views
Unification Algorithm without Occur Check
I have been reading about Unification algorithm here https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm
. And I wonder about the importance of occur check.
I know ...
2
votes
1answer
31 views
Convert propositional logic formulas to mathematical constraints
Brief introduction
In all boolean (or more generally mixed-integer) linear programs, constraints are represented as a matrix $A$, a support vector $b$ and is computed by $A^T x \leq b$, where $x$ is ...
1
vote
0answers
19 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).
...
2
votes
0answers
32 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
1answer
34 views
Programming in Propositional Logic article notation question
I was reading this article about propositional logic and transforming problems to SAT. The author often uses the following notation (taken from Dominating set section):
I don't understand what $[v,i]$...
2
votes
1answer
27 views
Definition of 2-CNF (a.k.a Krom) formula
In my lecturer's notes, the following definition for a 2-CNF wff is given:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is ...
0
votes
2answers
35 views
What if P implies Q is false when both P and Q are false?
This is actually a problem that our professor gave us, and I'm clueless of how to answer this. I browsed through various sources, but none were helpful regarding this question.
The question is,
In ...
0
votes
1answer
25 views
Embedded arithmetic set expressions
In set builder notation, we can represent the set: $$\{ 2, 7\}$$ as: $$\{ x | x=2 \vee x=7 \}$$.
Therefore, the PA arithmetic predicate: $$φ(x) := x=2 \vee x=7$$ is capable of representing this set....
0
votes
1answer
34 views
Representing a sentence using propositional logic
I am confused regarding a propositional logic representation of a sentence.
Please note that this sentence is not realistic:
"A person who is male (M) is smart (S) if he is tall (T), but otherwise ...
1
vote
1answer
35 views
Complexity of negation cancellation
Consider propositional logic over the connectives $\land$, $\lor$, and $\lnot$. Notation: $| \alpha |$ is the length of formula $\alpha$.
We are given a formula $\phi$. Cancel all cancellable ...
2
votes
1answer
25 views
Significance of quantifier ordering in quantified boolean formulas (kQBF vs. QBF)
I am studying solvers of quantified boolean formulas (QBF) as a generalization of SAT solving. The standard DIMACS format of SAT specification is extended to QDIMACS, which adds "a ..." and "e
..." ...
0
votes
1answer
40 views
How to correctly negate a predicate bounded by some quantifiers?
this is a problem which was asked in GATE CS 2010.
This is question statement:
Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
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 ...
1
vote
1answer
97 views
The optimized numbers of variables and clauses to encode a graph coloring problem in CNF
Problem Statement
Given a finite graph $G = \langle V, E\rangle$, consisting of vertice set $V$ and edge set $E$, and a finite set of colors $C$, a problem instance of graph coloring is to assign ...
2
votes
1answer
34 views
Non-Boolean SAT
I was wondering about the complexity of SAT tests with variables $x_i = 0 \lor 1 \lor 2 \dots \lor n$, with clauses being of the form $x_i = a \implies x_j \neq b$. When $n=2$, we have 2SAT, which has ...
0
votes
2answers
54 views
prove that {$↔,⊕$} is incomplete set?
How do i prove that Is {$↔,⊕$} not a complete set ? I have no clue how to prove it .
3
votes
1answer
108 views
Are these 2 equivalent?
Is ∀x∀y∀z[φ(x,y)∧p(y,z)->p(x,z)] equivalent to ∀x∀y∀z[φ(x,y)∧p(x,z)->p(y,z)] ?
The only thing I can think of is that this question can be answered if we show that ...
0
votes
2answers
63 views
Does the naive conversion of a Boolean Formula to CNF have a polynomial or exponential complexity?
I am reading the naive conversion to CNF, this procedure is explaining in this book book, but I have not found a conplexity analysis of this algorithm:
elimination of equivalence
Elimination of ...
0
votes
0answers
51 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
63 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
105 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
73 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
59 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
80 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
72 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
110 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\...
4
votes
0answers
43 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
31 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
26 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
61 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
211 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
77 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
160 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
68 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
46 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
43 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
73 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
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.
...
2
votes
1answer
47 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
214 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
38 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 ...
2
votes
1answer
184 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
72 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
193 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
295 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
82 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
44 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
35 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
68 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
66 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):
...
