Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
942
questions
1
vote
1
answer
10
views
What is the proper way to write logic formula, say concerning graph theory?
Say for example I'd like to state that there exists a pair of vertices such that they form an edge in one graph but not some other graph. I'd go about it as follows:
$$ \exists u, v \in V, (u,v) \in G,...
- 631
-3
votes
0
answers
15
views
Binary Sequence
Computer is used to control security lights given as 0110010. The system is programmed in that there will be light when 10101010 trigger switch is activated while switching signal is given as 01010. ...
0
votes
1
answer
57
views
Is "Bitwise Complement Operator" (~ tilde) distributive?
To be more precise, Is ~(a+b) = ~a + ~b? Here, "~" bitwise NOT operator.
I ran into this question while thinking about ...
- 1
0
votes
1
answer
30
views
Logic for Computer Science - How to define msort, merge and split functions inductively?
In "Modelling Computing Systems: Mathematics for Computer Science", I came across a logic exercise to inductively define a merge sort function 'mergeSort', with a hint to first define ...
0
votes
0
answers
19
views
Constrained Horn Clauses vs. "ordinary" Horn Clauses
I see why ordinary Horn clauses (of the type Prolog might accept) are first order eg something like (with all variables universally quantified)
$$
P(x) \leftarrow Q_1(x),Q_2(x,y).\\
P(x) \leftarrow ...
- 262
0
votes
0
answers
13
views
Converting regular expression to WS1S formula
Is there a "textbook" procedure to convert a regular expression such as $((0,1)(1,0))^*$ to a formula in WS1S?
- 2,230
1
vote
1
answer
35
views
K in SKI combinator calculus: why doesn't it take one parameter since it ignores its second?
In the SKI combinator calculus, Kxy returns the constant function which always returns x. Since y is always ignored, why not just define K as having a single parameter, namely, x? What is the purpose ...
- 159
2
votes
1
answer
45
views
Safety VS. Liveliness Property
I have to prove whether a certain property is safety or liveliness. The property represents the absence of deadlock so I expected it to be a safety property from what I read online.
The issue is that ...
- 121
1
vote
0
answers
25
views
Relational calculus: "Find all X with at least y amount of Z"
Assuming I have two relations:
Supplier [ID (PK), Name, City, Country] and
Item [ID (PK), Name, Department, Price, Stock, Supplier_ID (FK)]
What would be the easiest way to determine the following ...
- 11
0
votes
1
answer
49
views
Using hypercomputation for "impossible" problems?
In mathematics and philosophy there are some unsolvable problems like Russell's paradox or the liar's paradox that are usually said to be undecidable... There are also other "impossibilities"...
- 101
1
vote
1
answer
34
views
Proof that propositional resolution is refutation complete
I am studying theoretical computer science and I am in the part about resolution in propositional calculus. I was reading a theorem (and its proof) that propositional resolution is refutation complete,...
- 290
0
votes
0
answers
33
views
Complement of a language definition
Let $A=\{$ M is a TM, $s\in \mathbb{N}$ and $\exists x\in\Sigma^*$ s.t M rejects $x$ in at most $s$ steps $\}$.
I want to define its complement, so how do I negate "$\exists x\in\Sigma^*$ s.t M ...
- 21
-4
votes
2
answers
27
views
Let F be a function defined for all nonnegative integers by the following recursive definition
Let F be a function defined for all nonnegative integers by the following recursive
definition.
F(0) = 0, F(1)= 1
F(n + 2) = 2F(n) + F(n +1), n>0
Compute the first six values of F; that is, write ...
- 1
0
votes
0
answers
20
views
Hoare Logic - Interpreting identity
I'm having some issues on understanding the following identity:
{ P } S { Q } ≡ [P ⇒ wp.S.Q]
Does this means that if I have something like:
...
- 1
0
votes
0
answers
26
views
Minimum DNF length of a conjuction of equivalences
Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses.
I am puzzled on what approach to take -- whether to ...
- 109
0
votes
2
answers
31
views
Logical equivalence priority
I have the logical formula
$$
A \Leftrightarrow B \Leftrightarrow C
$$
In order to make the truth table I'm not sure wheither I should interpret it as
$A \Leftrightarrow B \Leftrightarrow C$ or $A \...
-1
votes
1
answer
58
views
Does quantum computing imply LPO?
The binary expansion of a given real number can be encoded as an amplitude using the inverse QPE. Together with Amplitude Amplification, I wonder if this could indicate that the (some weakened?) ...
1
vote
2
answers
44
views
"Largest set" in coinductive definitions
In several explanations of coinductive definitions (for example, in the answers to What is coinduction?), we're told that while an inductive definition gives us the smallest set with a specified set ...
- 936
1
vote
0
answers
51
views
Method for simplifying complex logic tables
Not sure if this is the right StackExchange site, but back in college (20 years ago) I took a Digital Systems Design class where we learned how to reverse engineer a boolean function to meet the ...
- 111
0
votes
2
answers
37
views
Boolean Logic when one component switches from 0 to 1
I recently was constructing boolean logic for all sorts of examples from Morris Mano's "Digital Logic and Circuit Design".
I noticed that it is possible to construct a boolean logic wrt the ...
- 1
0
votes
0
answers
30
views
Can you help me confirm this proof is valid for the Sequence Alignment lemma?
I'm reading the text Algorithm Design by Jon Kleinberg and Eva Tardos. In Chapter 6, the dynamic programming chapter, they discuss the Sequence Alignment algorithm and its importance to computational ...
- 101
1
vote
7
answers
186
views
How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?
I know that Quicksort or MergeSort are faster than, say, Bubblesort or Selection sort. And I know why (complexity metrics) but I never been able to find out how could someone start with, for example ...
- 113
-2
votes
1
answer
37
views
How to round numbers to its 0.5 superior in python
So basically my question is if i have for example 2.2 i need to create a python function to round numers to its higher 0.5 part, i mean
2.2 --> 2.5
2.3 --> 2.5
2.5 --> 2.5
2.6 --> 3
I cant ...
- 1
0
votes
1
answer
58
views
What defines a byte?
I am asking this question because for some reason ascii codes from range 128 - 255 have a size of 2 bytes but their composition is 8 bits which makes them a "...
- 23
1
vote
0
answers
28
views
Are there systems in computer science where we have several logic systems working all at once and without isolation?
Are there systems in computer science where we have several logic systems working all at once and without isolation? I am thinking there are system where subsystem A uses Paraconsistent logic, ...
- 109
1
vote
1
answer
59
views
Simple Skolemization Question
Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
0
votes
1
answer
78
views
If computers only work with intuitionistic/constructivist logic, so how it works with binary code?
Constructivist mathematics states that in order to prove something, we must construct this something, in a notion similar to computation, where things don't spring out of nowhere from some "...
0
votes
0
answers
35
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
145
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
50
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
50
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
33
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
45
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
0
votes
0
answers
41
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
102
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
1
answer
86
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,...
- 11
0
votes
1
answer
116
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
108
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
38
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,393
0
votes
0
answers
36
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
39
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))$$
- 121
1
vote
0
answers
33
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
40
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
194
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
46
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
28
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 ∧ ...
- 631
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
25
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