Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
925
questions
0
votes
2
answers
28
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
27
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
168
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
32
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
57
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
22
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, ...
- 111
1
vote
1
answer
45
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
73
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
125
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
38
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
27
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
41
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
39
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
75
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
84
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
51
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
92
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
34
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
32
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))$$
- 117
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
34
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
192
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
45
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
26
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
23
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
58
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
28
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
134
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
115
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 ...
user148883
0
votes
0
answers
72
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
69
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
66
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
39
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
30
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
25
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
38
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
179
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
46
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
31
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
103
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
43
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 ...
- 143
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