Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
839
questions
1
vote
1answer
54 views
Number of substrings possible with even characters
Consider a string 'ABBAA'
Possible substrings with even number of characters are $4$
'ABBA' : Count of 'A' is even and 'B' is even
'AA' : Count of 'A' is even and 'B' is even - ($0$)
Similarly 'BB' ...
4
votes
2answers
68 views
How do computers *really* work? (at the most basic level)
While learning about computers I will read about RAM and Storage and the CPU, and while these explain the architecture of a computer and how parts of a computer work together, I still don't understand ...
1
vote
1answer
18 views
Proving using a SAT solver that KB entails D
Suppose you're given this KB:
$$KB = (A, A ⇒ B, A ⇒ C, B ∧ C ⇒ D)$$
How would you show using a SAT solver that $KB \vDash D$?
0
votes
2answers
35 views
Oracle that can only definitively say if an instance is unsatisfiable
Assuming I have an Oracle that takes as input a strictly 3SAT Boolean instance and states whether the instance is satisfiable or not. If it says instance is unsatisfiable then the instance is ...
1
vote
1answer
29 views
Number of substrings with exactly k distinct characters
Given a string s and an int k, return an int representing the number of substrings (not unique) of s with exactly k distinct characters. If the given string doesn't have k distinct characters, return ...
1
vote
1answer
25 views
Showing that a bijection preserves homomorphism
I have the vocabulary $\tau = \{+, 0 \}$ and the structure $R = (\mathbb{R}, +^R, 0^R)$ where $+^R$ is a binary function symbol representing the normal addition of numbers and $0^R$ is the constant $0$...
-6
votes
0answers
40 views
Two Statements and Conclusions: Which Choice is Logically Correct? [closed]
This is a question asked in GATE 2021. The problem is in C and D options. If one interpret question in different ways both C and D can be correct. Can someone clarify?
Two statements and conclusions ...
0
votes
2answers
78 views
Encoding the theorem on friends and strangers in predicate logic
In every group chat of six (distinct) people on Instagram, there is a group of three (distinct) people such that either:
everyone in the group are friends
everyone in the group are strangers (i.e not ...
3
votes
0answers
24 views
CTL and the modal mu-calculus
Is there any literature / results to which fragment of the modal mu-calculus the logic CTL corresponds? I know that in order to tranlsate the until operators of CTL, it suffices to use a single mu-...
0
votes
1answer
27 views
Converting into CNF
I am still a bit confused by how to convert into CNF even though I have the rules written down.
How do I convert the following sentence into CNF?
$(I \lor M) \Rightarrow H$
I know I need to get rid of ...
1
vote
0answers
28 views
Multiple parameter predicates and the Relational Model
I've got a very general question about the relational model and it's relationship to 1st order predicate calculus. It will probably seem very basic to most, I'm afraid, a consequence of me grappling ...
1
vote
2answers
31 views
Propositional Logic: Entailment
Given the sentences, S1, S2, if S1 |= S2 then all models that satisfy S1 also satisfy S2, how is the following statement correct?
A ∧ ¬A |= B
How can something and ...
0
votes
2answers
45 views
In propositional logic how is the negation equivalent?
I am unable to understand how the negation of a sentence into CNF actually makes sense, hopefully somebody can explain it to me in understandable terms!
Given the sentence: If the battery is charged (...
0
votes
0answers
39 views
A necessary condition for a relation to be in 2NF but not in 3NF is that some non-prime attribute must be determined by a non-prime attribute
I will state the complete question now, since it did not fit in the title.
Is the statement given below correct?
A necessary condition for a relation to be in 2NF but not in 3NF is that some non-...
2
votes
0answers
37 views
Is there a diagram of related logics?
Proving software is based on logics and there any many logics. AFAIK all of the logics can be shown as a tree diagram of how they are related; for example, a tree of how types of number are releated
...
4
votes
1answer
50 views
Proving equivalence of two substitutions by induction
I'm trying to prove the following reduction:
$$
t\{x:=u\}\{y:=v\} = t\{y:=v\}\{x:=u\{y:=v\}\}
$$
under the following assumptions:
$x \neq y$
$x$ is not a free variable of $v$ (in symbols, $x \...
3
votes
1answer
56 views
What's the average number of transistor switches needed to do an N-bit x N-bit multiply?
I want to know how switch-efficient a multiplier can be. If I need to do many $N$-bit by $N$-bit multiplies, and each bit is determined by flipping a coin, what's the average number of transistor ...
2
votes
1answer
38 views
Clarifying the definition of reduction with regards to NP-complete problems
In my logic class we started learning about the different complexity classes. In particular, we focused on the NP complexity class. A problem is in NP if it is solvable in polynomial time using a ...
2
votes
0answers
338 views
Prove that PRE-WORK-POST is Turing Complete
This is a homework question and I am trying to fully understand what I have to do and how to go about it. Therefore, I don't want full answers to the question.
The programming language PRE-WORK-POST ...
4
votes
0answers
36 views
Do FOL theorem provers accept axiom schemata?
Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata?
I looked in the Vampire "manual" briefly,...
-2
votes
1answer
23 views
Consider 4 positive integers a,b,c,d having exactly 10^11 bits (considering the leading zeroes) in the binary representations
Consider 4 positive integers a,b,c,d having exactly 10^11 bits (considering the leading zeroes) in the binary representations. Positions are numbered from 1 to 10^11. Every 3rd bit of a is equal to 1 ...
0
votes
0answers
21 views
Comparing Registers with 16-bits
I am given with this information:
"CMP OP1,OP2 will compare registers OP1 and OP2 if they are equal,
flag values will be ZF=1, CF=0,
if the first
operands value is greater flag values will be ZF=...
0
votes
2answers
64 views
A basic question about predicate logic
Suppose we have a statement: "Tom has a car" and we have an auxiliary clause that is
has(x, y): x has y then to write the statement in logic I am guessing ...
0
votes
1answer
37 views
An equivalent of $\neg ((a \wedge b) \Leftrightarrow c)$ based on a specific requirement
I am solving a problem that is asking to provide an equivalent for $\neg ((a \wedge b) \Leftrightarrow c)$ and the equivalent shouldn't contain $\wedge$ (and), $\Rightarrow$ (implication) or $\...
0
votes
0answers
42 views
What is the difference between type theory and logic programming (in terms of declarative programming and specification)
How is does type theory (coq, lean, agda), and logic programming (prolog, datalog) differ from each other.
Logic programming is a way of declarative specifying an algorithm, using classical 1st order ...
0
votes
1answer
26 views
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
a. Decidable
b. At least expressive as propositional logic
c. NP-complete
a) Decidable: no, some first order ...
0
votes
1answer
31 views
Create an Finite Deterministic Automata for a regular expression
I want to create a finite state machine that accepts the following language:
$$
L=\{w\in\{a,b\}^* | w \text{ contains abb but not on the first position}\}
$$
So I began by writing a regular expression ...
0
votes
1answer
40 views
Is Conjunctive Normal Form or not?
I have one formula that I do not understand why it is CNF and one that is not CNF, namely.
p && !q (NOT NCF)
and
!!p(CNF).
According to the exercise where I found these examples, 1 is not ...
0
votes
0answers
19 views
Is my UML Use Case Diagram valid?
I'm preparing an UML use case diagram for my following school project:
...
1
vote
0answers
35 views
Help me understand whether these critical pairs are joinable
I have the following TRS $R$:
$$
l_1 = f(g(x)) \to f(x) = r_1 \\
l_2 = g(f(y)) \to g(y) = r_2
$$
I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$.
I have ...
1
vote
0answers
50 views
Why is most research in logic and verification conducted in Europe rather than the US?
This is the CSRankings output for logic and formal verification for the last 10 years, worldwide:
http://csrankings.org/#/index?log&world
For the International Conference on Computer Aided ...
0
votes
0answers
12 views
How to combine multiple Boolean Functions in CDNF efficiently for implementation on a CPU?
I am trying to see how fast I can implement a 6-bits to 6-bites lookup table. Generally, I am attempting to do this by using the common method mentioned in CS textbooks of using the Quine-McCluskey ...
0
votes
0answers
20 views
Prove the boolean function E = F + G contains of the sum of the minterms of F and G
I'm given a boolean function E which is result of the sum of F and G (Where both F and G are boolean functions for sure).
By using K-Map I can easily understand why E would have the sum of the ...
0
votes
1answer
32 views
is duality principle in boolean algebra is true for every expression
Let say A = 1 and B = 1
and then A+B = 1
now by using duality(replacing or gate by and gate and 1 by 0) we can say that, A.B = 0
but this is not 0, because 1.1 = 1, so please anyone clear my ...
2
votes
0answers
22 views
Automated algorithm design
There is a huge field of study dedicated to automated theorem proving. Is there any similar research dedicated to automated algorithm design? And is there any form of "duality" between these ...
0
votes
0answers
36 views
Check if given safety properties are regular, and if so construct NFAs
Let $\mathit{AP} = \{a, b, c\}$. Consider the following LT properties:
Between two neighboring occurrences of $a$, $b$ always holds.
Between two neighboring occurrences of $a$, $b$ occurs more often ...
1
vote
0answers
33 views
Name for a function on formulae that does not break the structure of given formula
I have two logics, $L_1$ and $L_2$, and a mapping $f: Formulas_{L1} \rightarrow Formulas_{L2}$, and want to argue that the mapping is "nice", in the sense that it is structure-preserving. ...
4
votes
0answers
202 views
Can every sentence of first-order logic be converted into an equisatisfiable equation in Boolean algebra?
There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational ...
3
votes
2answers
89 views
How expensive is it to verify that a gate is universal?
I know that a NAND gate is considered universal because we can use it to implement an AND, OR, and NOT gate.
Given an arbitrary gate, or set of gates, how many operations would it take to verify if ...
0
votes
1answer
41 views
For a logic gate to be universal, must it necessarily be able to perform duplication?
It is said that a gate that can simulate AND and NOT is universal and able to recreate any classical circuit. I was looking at some of the circuits simulated by NAND, and for some of them, we need to ...
2
votes
1answer
25 views
first order logic to normal form order of operations
∃y∀x [A(x) ∧ B(y) -> C(x,y)]
∃y∀x [¬(A(x) ∧ B(y)) v C(x,y)]
∃y∀x [¬A(x) v ¬B(y) v C(x,y)]
I need to convert the above to conjunctive normal form. I'm a ...
-1
votes
1answer
56 views
1
vote
1answer
40 views
Universal Quantifiers in QBFs
I've been looking into reductions to/from the TQBF language and have managed to get stuck on something that is almost certainly not true (or, if it is true I'm missing a significant computational cost ...
0
votes
1answer
37 views
Lambda calculus simplification excercise
Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.
(λx.λy.yx)z (λw.w)
I am lost with this.
if anyone could lead me in ...
0
votes
0answers
23 views
Two variants of Fredkin gate
Sometimes two outpus of Fredkin gate are swapped when constant bit is 0, sometimes when it is 1. What variant is right or more modern? If it was conscious decision to change behavior what was ...
1
vote
0answers
25 views
In theory, should neuromorphic computers be more efficient than traditional computers when performing logic?
There is this general sentiment about neuromorphic computers that they are simply "more efficient" than von Neuman.
I've heard a lot of talk about neuromorphic computers in the context of ...
0
votes
1answer
26 views
Represent a DNF formula as a multivariate linear formula?
Lets say I have the following DNF: (x or y) and (z or i) / $(x\lor y)\land(z\lor i)$
How do I convert that into a polynomial form?
5
votes
1answer
40 views
Test two LTL expression trees for equivalence
Is there an algorithm on how to check if two LTL expressions (represented as binary trees) are semantically equivalent? Since there are many smaller equivalences such as
$a\Rightarrow b \equiv \neg a \...
0
votes
0answers
46 views
Building an ALU on nandgame's website
I'm working on nandgame's website found here. I'm working on the ALU and here is an image of my implementation:
My Implementation:
And I compared it to this website's solution:
Solution
However when ...
2
votes
0answers
48 views
Can HOL be simulated in the CiC?
I was wondering if HOL (higher-order logic) can be simulated in the Calculus of Inductive constructions (CiC)
