Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
917
questions
0
votes
0
answers
30
views
resolving in CDCL
When resolving in Conflict driven clause learning, it is the case that if you resolve a conflicting clause with the reason of the negation of one of his literals, then this results in another ...
- 55
2
votes
1
answer
115
views
Formal language rewrite rules: strange notation
I'm reading "Program=Proof" by Samuel Mimram, and they use a notation for defining a formal language that I'm not familiar with.
Here is how "Program=Proof" defines a formal ...
- 184
0
votes
1
answer
46
views
Boolean Logic for Floats
I would like to know whether a theory exists which generalizes boolean logic to floats.
Specifically, assume that instead of booleans 1 and 0, I have True/False tendencies, such as 0.9, where 0.1. ...
1
vote
1
answer
36
views
substitution of same variable in context-free grammars
Above is a theorem coming from the book "Formal languages and automata" by Peter Linz concerning substitution of variables.
Could someone explain why A and B have to be different variables?
- 55
0
votes
0
answers
19
views
Prove a Predicate is Primitive Recursive
Suppose $x$ is Godel's number of some formula. Predicate $\operatorname{P}(\operatorname{f}(x))$ is true only when the number of functions is equal to the number of predicates in that formula.
Prove ...
0
votes
0
answers
36
views
First-Order logic exercise
I'm trying to solve the following exercise:
Given this is true:
\begin{align} \neg \forall x \space \ \exists y \ ( x\neq y \rightarrow LeftOf(x,y) )\end{align}
Demonstrate :
\begin{align} \exists y \...
- 1
-4
votes
0
answers
72
views
2-Satisfiability is NP Complete, isn't it?
To show that any formal language is NP Complete first it must be showed that this formal language is both in NP and NP Hard.
So to show that 2-Satisfiability is NP Complete first it must be showed ...
0
votes
0
answers
37
views
Given a 2D Array (of 0's and 1's), find the minimum number of rows required so that maximum columns have their sum greater than a threshold
I have a 2D array of some rows and columns which are having only 0's and 1's. I would want to know if there is a way to optimize the number of rows so that maximum number of columns have their column ...
0
votes
0
answers
62
views
Horn Satisfiability is NP Complete, isn't it?
To show that any formal language is NP Complete first it must be showed that this formal language is both in NP and NP Hard.
So to show that Horn Satisfiability is NP Complete first it must be showed ...
0
votes
2
answers
71
views
Elemination of duplicate premise
Suppose that I have proof tree starting with some statement |- B in a sequent calculus, leading to two premises/leafs |- A.
Is it always possible to transform such a proof tree into another proof tree,...
- 1
0
votes
1
answer
42
views
How can I prove that LTL formula is valid?
I do not know with which technique i can prove if a LTL forumula is valid.
Let's say we have for example this one: ¬q U(¬p ∧ ¬q) → ¬Gp. How can prove if this valid or not? (should be true in any state ...
- 3
1
vote
2
answers
82
views
Combinational logic check if bits is prime
I wonder if there's Digital Logic Circuit (using combinatorial logic gates) that check if number is prime or not.
For example given input fixed 8-bit that will produce 1-bit output.
00000101 will ...
14
votes
6
answers
5k
views
Is it provably true/false that for a program, there exists a proof whether it halts or not?
A standalone statement of my question
Given a program that takes no argument, we are interested in whether the program will eventually terminate. My question is this:
Theoretically speaking, can we ...
- 188
0
votes
1
answer
33
views
Universal quantification and the number of solutions
How would one count the amount of solutions to quantified formulas that have universal quantifiers? For example, for a boolean formula $\Phi(X)$ with a number of solutions $\#\Phi(X)$ let's construct ...
- 1,381
0
votes
0
answers
28
views
How to mathematically convert an array of bytes to a decimal value
With C# I can convert an array of bytes to a decimal value:
...
- 101
1
vote
1
answer
20
views
How to come up with combination a short-circuit evaluation table?
(a || b) || (c && d))
Given the above, how do I derive the table below:
a
b
c
d
output
T
-
-
-
TRUE
F
T
-
-
TRUE
F
F
T
T
TRUE
F
F
T
F
FALSE
F
F
F
-
FALSE
I'm told that this is short ...
- 11
1
vote
1
answer
38
views
What does :: indicate in all-quantifier predicates?
Can somebody explain to me the meaning of $::$ in the following predicate?
$$(\forall i : P(i) : Q(i)) \equiv (\forall i :: P(i) \implies Q(i))$$
- 115
1
vote
0
answers
31
views
Is it coherent to treat the C programming language as a formal system? [closed]
This is cross-posted from a similar question on Mathematics Stack Exchange, on the advice of a commenter.
In mathematical logic, a formal system is a structure which includes, amongst other things, a ...
- 111
0
votes
1
answer
23
views
How to converts Pseudo boolean constraints to cnf format?
How to convert Pseudo boolean constraints to CNF format
for example L1 + … + Ln ≥ 1 is converted to L1 ∨ … ∨ Ln
but how about:
L1 + … + Ln ≥ k
L1 + … + Ln < k
or
L1 + L2 = k
or
2 L1 + 2 L2L3 + L4 ...
- 25
1
vote
2
answers
190
views
Logical consequence problem, doubt
It is possible to have this logical consequence?
$$
\forall x (p(x) \vee q(x)) \models \forall x p(x) \vee \forall x q(x)
$$
- 13
1
vote
1
answer
40
views
Why we can't use deduction theorem on soundness to contravene second incompleteness with lob's theorem
I'm starting to learn modal logic and there is something that's bothering my mind for a while.
we know from deduction theorem that $((\vdash q) \rightarrow (\vdash p)) \Leftrightarrow(\vdash (q \...
1
vote
0
answers
24
views
What knowledge do players $y_1$ and $y_2$ have exactly in this example for Dependency Quantified Boolean Formula?
In [1], the authors give the following example to explain how Dependency Quantified Boolean Formulas (DQBF) work:
As an example for a DQBF, consider the formula
$∀x_1∀x_2∃y_1(x_1)∃y_2(x_2) : (x_1 ∧ ...
- 582
0
votes
0
answers
19
views
Algorithm to Detect Disjunctive Relationships
I'm working with logic formulas of the form '0 & 2 | 0 & 3'. I was wondering if anyone knew of an algorithm that would take in such a formula, detect existing disjunctive relationships, and ...
- 1
0
votes
0
answers
21
views
Creating a new list with with every other element
I am new to Isabelle, I am looking for a way to extract every other element of a list into a new list. Similarly, how do I extend it to extracting every 3rd element of a list?
For example, given [1,2,...
- 1
0
votes
0
answers
19
views
How to specify in Isabelle that there exists j in an interval
I am looking to specify something in Isabelle of the form that there exists a $j$ such that $lb < j < ub$, where $lb$ and $ub$ are lower and upper bounds.
For a single condition, we can say, for ...
- 1
2
votes
1
answer
56
views
Is $f(X)f^d(X) = 0$ for a Boolean function $f$?
I'm currently trying to understand a step in the proof for in the Crama and Hammer book on Boolean Functions. The proof is Proposition 4.12, which claims that the self-dualization of Boolean $f$ is ...
- 419
1
vote
0
answers
27
views
How do I prove the following invariant of this program?
I have been studying different topics within the realm of concurrent programming and came across "Lamport's bakery algorithm" which is based on the original version of the bakery algorithm ...
- 131
10
votes
4
answers
5k
views
Could Gödel’s incompleteness theorem be circumvented with a quine?
As you all probably know, Gödel’s incompleteness theorem states, that it will never be possible for mathematics to prove its own correctness.
Mainly because that proof would be part of mathematics too,...
- 225
3
votes
1
answer
125
views
Building non-classical logics in Agda & Coq
Is it possible to construct different systems of logic in Coq or Agda?
I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, ...
1
vote
1
answer
114
views
Proving a predicate assignment is correct
I am currently reading Formal Methods - An Appetizer and am stuck in chapter 3 (Program Verification).
I am unfamiliar with logic and I do not think I understand the $\vDash$ notation correctly.
I ...
- 13
0
votes
0
answers
43
views
Logic Gates - 3 Sensors in a Factory
I am studying logic gates and I encountered this problem:
A set of three sensors in a factory detects whether the pollution level it is
outputting from an incinerator exceeds the safety limit. In ...
- 111
0
votes
2
answers
64
views
Is there a quantifier more powerful than the other to determine FOL connector?
So basically we have 2 types of quantifier in first order logic, they are universal quantifier and existential quantifier. Usually we use implies connector(->) when we have universal quantifier in ...
0
votes
0
answers
53
views
Set, then get, or first get, then set?
In some abstract programming languages there is a concept "setter and getter".
Generalizing, should this be the opposite, i.e. "Getter and setter"?
I would theorize that one should ...
2
votes
0
answers
37
views
Reading list for mathematics and formal logic with missing truth values?
I would like a reading list of math and formal logic books which give a principled discussion of missing values.
Textbooks on mathematics and formal logic - propositional and first-order and higher-...
- 163
0
votes
0
answers
28
views
Is there an efficient way to generate a pseudo-boolean function from a linear constraint?
I would like to define a pseudo-boolean function $f$ such that $f(x) = 0$ for all logically valid combinations of $x\in{0,1}$ and $f(x) > 0$ for all logically invalid combinations of $x\in{0,1}$.
...
- 121
0
votes
0
answers
23
views
how would i go about creating a base 10 to base 2 converter
I am trying to create a calculator in excel for use in Minecraft later and I was wondering if the was any way to create and how I would create a base 10 to base 2 converter with only logic gates. if ...
0
votes
1
answer
35
views
How do logical and bitwise operators work on numbers? (e.g "2 and not 5")
====TLDR=============================================================
Curious about the behaviour of logical and bitwise logical operations on integers, i.e with
and...
0
votes
0
answers
141
views
8-bit binary to bcd converter Verilog
We have been given task to write a 8-bit binary to bcd converter Verilog code, using structural code NOT behavioural, is it possible to guide us how can we create 8-bit binary to bcd converter using ...
3
votes
1
answer
43
views
Stalmarck's method: x ≡ x → z, does z have to be true?
I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:
y $\to$ z $\equiv$ x
where x, y and z are booleans which ...
- 53
-1
votes
1
answer
27
views
Conjuctive Normal Form
Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if
Q and R have different truth-values; or
P and R have the same truth-values.
Choose all formulas that are in conjunctive ...
2
votes
2
answers
101
views
What if solving P vs NP revealed a contradiction?
Let's just say that some person discovered that $P = NP$ implies $P \neq NP$ and $P \neq NP$ implies $P = NP$, and we don't know what is causing this contradiction, And this was a valid proof that was ...
- 99
2
votes
1
answer
42
views
Resolution algorithm does not seem to generate the empty clause
Let's assume I have the following 3 clauses:
$\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$
and I want to see if our KB entails $\neg U$ so I tried to apply ...
- 43
0
votes
0
answers
167
views
Construct CFG of monadic logic
How to construct CFG for tautologies in monadic predicate logic in the empty model. The predicates are Q and P, operations are ...
- 3
3
votes
1
answer
49
views
CTL trouble translating text into formula
I have an excercise where I have to translate verbally formulated statements into CTL formulas. I have particularly trouble with this one:
On every path q is true at least once and p was true ...
- 135
1
vote
0
answers
17
views
Proving set of register machines that halt before k steps for some input is non-recursive
Given an enumeration of register machines $R_n$ that take a single natural number as input, and a constant $k$, the function $f$ is defined as:
$$
f(n) = \begin{cases} 1 & \exists m \text{ such ...
- 11
0
votes
0
answers
29
views
Specific quantifier elimination for real algebraic numbers
It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
- 113
3
votes
3
answers
152
views
How many possible arithmetic operations are there between two N-bit numbers?
It's generally considered to be the case that there are sixteen possible logical operations between two N-bit numbers and four possible logical operations on one N-bit number. I'd like to know how ...
- 81
1
vote
1
answer
66
views
Translating Natural Language to LTL Formulae
I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct.
I'm given the sentences, and my assumption is that $l$ ...
- 111
0
votes
1
answer
53
views
Domain of discourse vs First-order theory
In the question (Validity of predicate logic formulas) I see the following way of expressing:
"The predicate $P(x,y) \equiv \bigl[ y \cdot x = 1 \bigr]$, where the domain of discourse is $\...
- 113
0
votes
1
answer
23
views
Determine if the following arithmetics are sentences
How would you determine if these arithmetics are sentences or not?
-(x + 2) > y
i++ == 2
i++ == 2 is this sentence True where i = 1
I understand it as if the ...
