Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
1,020 questions
1
vote
0
answers
38
views
A confusion about Karnaugh Map
Consider the following four variable Boolean function:
$$F(A,B,C,D)=\sum(0,2,3,5,7,8,9,10,11,13,15)$$
If I show you the map, then what I get is:
I have marked the Essential Prime Implicants with a ...
- 111
1
vote
1
answer
43
views
Where is the Substitution Theorem used in the following example?
While going through the lecture notes on propositional logic, I came across the following example which proves that $(P \vee (Q \vee R) \wedge (R \vee \neg P)) \equiv R \vee (\neg P \wedge Q)$:
\begin{...
- 169
0
votes
0
answers
11
views
How do you express subtyping in multi-sorted equational algebraic theories?
I was told this is achieved with injective functions. Thus, the ordinal numbers can be mapped to a particular set in the type Set. But how do we express which one to map them to?
We only have ...
- 162
2
votes
0
answers
79
views
How might a fuzzy logic rice cooker actually use fuzzy logic?
This rice cooker purports to use Advanced Fuzzy Logic.
I understand it's hard to know how this specific rice cooker works, so my question is how might fuzzy logic for a rice cooker work in general? ...
- 378
1
vote
2
answers
57
views
Is this LTL formula really valid?
Fp → (¬p U p)
What if I have a transition system in which p is always true? Then Fp would be valid but not (¬p U p), right?
This formula is claimed to be valid in my study litterature, what have I ...
0
votes
0
answers
54
views
Help with writing an algorithm
I'm not sure if this question fits the forum, and I should mention that I'm not a computer scientist at all—just a regular normal boy with very little coding knowledge.
But I wanted to ask if it's ...
- 1
1
vote
1
answer
77
views
How to make a NAND gate with vaccum tubes?
We all know the NAND gate with mosfets. However, a lot of history of computers is unknown. Can you please let me know a diagram of a NAND gate with mosfets how is it made with vacuum tubes or a ...
1
vote
1
answer
43
views
Is Monotone Not-Exactly-1 3SAT solvable in polynomial time?
I'm studying different variants of the SAT problem, and I came across the Monotone Not-Exactly-1 3SAT problem.
Specifically, this problem involves determining whether a Boolean formula in CNF, where ...
2
votes
1
answer
32
views
Are all solutions to a HORN-SAT problem required to contain the minimal model as a subset?
I'm studying HORN-SAT problems and I have a specific question about the minimal model.
Given a HORN-SAT problem with multiple solutions, I understand that the minimal model is the one with the ...
1
vote
1
answer
54
views
is 3-SAT ∈ NTIME(n^3)?
I'm struggling to understand the time complexity of 3-SAT using a non-deterministic Turing machine, as well as the relationship between NTIME and DTIME
For example, let's say we have 2 literals. My ...
- 13
0
votes
0
answers
26
views
Why are the x86 registers ordered A, C, D, B?
I figure there must be a practical reason, maybe something regarding the optimization of hardware, but I am curious for a definitive answer. When a ModR/M byte references a registry, it is done in the ...
- 1
2
votes
1
answer
73
views
How to show that $M$ is not finitely axiomatizable in the following case?
Problem: A set of formulas $M_0$ is an axiom system for a set of formulas $M$ if $\{A |A \text{ is a model for }M_0\} = \{A |A \text{ is a model for }M\}$, where $A$ is an assignment, or valuation. $M$...
- 169
0
votes
1
answer
50
views
How would I prove implications of this structure?
Consider the following to prove: $(A \implies B) \implies (C \implies D)$
Could this be proved by assuming A then proving B, then using A and B to prove C, then using A, B and C to prove D? or would ...
- 173
1
vote
2
answers
44
views
Why is $\phi[\top / q] \vee \phi[\perp / q] \equiv \phi$?
I'm pretty confused by the use of this equivalence in the induction proof for the Craig's Interpolation Theorem. In the equation, $\phi$ is a formula, and $q$ is an atomic formula in $\phi$, with $\...
- 169
2
votes
1
answer
56
views
Why $\models (F \rightarrow G)$ when $F$ and $G$ share no atomic formulas implies that either $F$ is unsatisfiable or $G$ is a tautology?
I encountered this problem when studying Uwe Schoning's Logic for Computer Scientists. At the moment, I simply don't seem to think the statement makes sense.
What I've tried is to suppose that it is ...
- 169
2
votes
2
answers
54
views
Does modifying input space change space complexity?
The auxiliary space analysis that involves modifying the input array can lead to "unfair" situations. Examples:
Consider that an algorithm that uses O(N) memory and does not need to ...
- 43
1
vote
0
answers
35
views
Sparse bit string pattern matching
Suppose there are two strings of bits. Let's call them the needle (n) and the haystack (h).
We'll say that the needle matches ...
- 111
1
vote
1
answer
81
views
MSOL for a vertex-cover enlargement problem
Consider the following problem.
Given a graph $G=(V,E)$, and two positive integers $k$ and $\gamma$, decide if there is a set of new edges to be added such that $|E'|\le k$, and any subset $V'\...
- 555
0
votes
0
answers
14
views
Question about PNF equivalency in sub-models
I'm given this formula: $\forall x(\forall zR(x,z)\rightarrow\exists yR(y,x))$.
Now, the statement that this formula is not logically true in every sub-model of a model that makes it logically true, ...
0
votes
0
answers
41
views
Why are languages fed as input into machines/automata as a stream and why do automata read one symbol at a time?
Consider an FSM augmented with a camera. The input is a book. First, the book is already stored without the FSM needing to have states to memorize the input. (The memory used to record the input is no ...
- 326
0
votes
0
answers
11
views
Counterexample Construction and Translation in CEGAR
As in this slide,
M2 is an abstraction of M1 using the abstraction function f1 which essentially groups based on labels. Then we see that the property is not satisfied by the abstraction so we find ...
- 90
0
votes
0
answers
23
views
When does Simulation Equivalent imply Bisimulation
Here, Given 2 Kripke structures M1 and M2, if there exists a simulation from M1 to M2 and a simulation from M2 to M1, is there a bisimulation from M1 to M2?, it is shown that for two LTSs M1 and M2 ...
- 90
2
votes
1
answer
132
views
Can CTL* express every model's behaviour
CTL* as in https://en.wikipedia.org/wiki/CTL*, is a logic that combines CTL and LTL. I know that CTL* can express everything expressible in these two languages and more. My question is whether we can ...
- 90
0
votes
1
answer
29
views
Linear Time properties classification
I know LT Properties can be classified with classes Invariants, Safety Properties, Liveness Properties as in https://en.wikipedia.org/wiki/Linear_time_property. My question is, does this cover all ...
- 90
1
vote
2
answers
62
views
Is there a linear programming method that is polynomial in the number of variables, constraints and bitlength of numbers?
AFAIK, Interior Point method for solving a system of linear inequations is polynomial in the number of variables and constraints. Probably there are others. I don't need to optimize any function (...
- 155
3
votes
1
answer
105
views
Can remainder mod 2 be efficiently computed from addition and equality?
Suppose I have a programming language all of whose variables have natural number type. (So I cannot form higher-type objects, e.g., lists or trees, of natural numbers.) The only atomic commands I am ...
- 131
3
votes
1
answer
615
views
Can the minimisation operation be seen from a programming language perspective?
If $f$ is a total function $\mathbb N^k\to\mathbb N$, and $g$ is a total function $\mathbb N^{k+2}\to\mathbb N$, then we say that $h:\mathbb N^{k+1}\to\mathbb N$ is definable by primitive recursion ...
- 133
0
votes
0
answers
34
views
How can I know the complexity of my conceptual game and solving it with an algorithm?
I made a really simple card game where you and your opponent have 6 cards and in a turn you can use only one of them and it will be discarded.
The cards have a value and an effect.
The cards, with ...
1
vote
0
answers
45
views
Analog of semantic paradoxes in type theory?
By semantic paradoxes, I mean like the Liar paradox, Curry paradox, Knower paradox, etc.
In classical (logic) settings, we would need to extend the language with a predicate P (truth or is-known ...
- 246
1
vote
0
answers
39
views
How could higher-order Datalog be more expressive than first-order Datalog?
According to this paper [1], higher-order Datalog is more expressive:
... we demonstrate that on ordered databases, for all k ≥ 2,
...
- 505
0
votes
1
answer
82
views
P=NP? A reduction of CNF boolean satisfiability to the circulation problem in an undirected graph
The picture below shows how to reduce the Boolean Satisfiability problem in CNF to the circulation problem in undirected graph (see here).
As you can see, a[i] are ...
- 155
1
vote
2
answers
43
views
Can a Code Script be Optimized for Time and Space Complexity Using Logic Gates
let's say that I have a Python script that performs various operations, including data manipulation, conditional logic, and iteration. However, I'm concerned about its time and space complexity ...
- 11
4
votes
0
answers
76
views
Extending Fagin's Theorem to the Polynomial Hierarchy
Fagin's Theorem (see Wikipedia and these lecture notes) states that there is an equivalence between second-order logic (SOL) formulas with existential quantifiers, and problems in NP.
I was wondering ...
- 41
0
votes
0
answers
35
views
Page miss in 2Q Cache Replacement
I am studying about 2Q Cache Replacement Policy and i came across this post.
They have worked out an example with the following page keys [1, 2, 3, 4, 1, 2, 5, 1, 2, 3, 4, 5] and cache memory of 5 ...
user167287
2
votes
0
answers
80
views
Prove or disprove that the Quine-McCluskey method generates the circuit with the minimum inputs and minimum gates?
Recently, when I self-learnt Discrete Mathematics and Its Applications 8th by Kenneth Rosen, it says in 12.4 Minimization of Circuits which uses the Karnaugh Map or the Quine-McCluskey method:
...
- 203
0
votes
0
answers
45
views
Do these courses fall under theoretical computer ccience [duplicate]
I am planning to apply for master's degree at TU Berlin and have to take some courses on theoretical computer science since the university requires me to take some credits on theoretical computer ...
- 1
0
votes
0
answers
51
views
Do these courses fall under theoretical computer ccience
I am planning to apply for master's degree at TU Berlin and have to take some courses on theoretical computer science since the university requires me to take some credits on theoretical computer ...
- 1
0
votes
0
answers
22
views
Do these courses fall under theoretical computer ccience [duplicate]
I am planning to apply for master's degree at TU Berlin and have to take some courses on theoretical computer science since the university requires me to take some credits on theoretical computer ...
- 1
0
votes
0
answers
17
views
Finding program that enumerates a language using Von Neumman's computability paradigm
Given an alphabet $\Sigma$ of $n$ elements, whenever there is some order $\leq$ over the elements of $\Sigma$, we define $s^{\leq} : \Sigma^{*} \mapsto \Sigma^{*}$ as
\begin{align*}
s^{\leq} \left(...
- 195
4
votes
1
answer
203
views
SAT formulation of the condition that an even number of a given set of variables must be set to true
Lets say I have a SAT problem with variables $x_1,...,x_n$. For a given subset of the variables I want to create a clause which forces an even number of the variables in $S$ to be true. Of course ...
- 225
1
vote
0
answers
60
views
Is it known, whether the complement of NP-hard problems is necessarily again NP-hard?
Neither could I find any counterexamples, nor could I show that if indeed the complement of NP-hard problems was NP-hard, one could deduce some unknown results from it, which would imply that it is ...
1
vote
0
answers
39
views
What logical system does hindley-milner correspond to, according to the curry howard correspondence?
If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
- 36
2
votes
2
answers
62
views
What is "the ability of classical control operators to return multiple times from a single term"?
I am puzzled by a point in this paper by Phil Wadler.
Figure 6 shows a proof of the law of the excluded middle, $A ∨ ¬A$. The computational interpretation of this proof exploits the ability of ...
- 341
0
votes
0
answers
45
views
Expressing Boolean Functions In Terms of Another Function
Given two boolean functions f1 and f2, are there any tools available that could be used to automate the process to represent f1 in terms of f2? I understand the process of this doing this by hand ...
1
vote
3
answers
183
views
Hoare Logic: Identifying Hoare Triple given a simple function
The program is designed to start with values for $x$ and $y$. The variables $u1$ and $u2$ are intended to represent $x$ and $y$ in ascending order.
Provide suitable preconditions and postconditions ...
- 11
1
vote
1
answer
58
views
(Co)-induction, fixpoints and inference systems
I'm learning about induction and co-induction. From what I know, given a set of judgments $U$ and an inference system $\Phi \subseteq \wp(U) \times U$, where $(\left\{ h_1,\dots,h_n \right\}, c) \in \...
- 13
1
vote
0
answers
42
views
How do I prove relations of two CTL formulas?
If I have two CTL equations, how do I prove they're equivalent or that one implies the other?
What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
- 326
1
vote
2
answers
61
views
Complexity of satisfiability for relational logic on the booleans
I know that propositional satisfiability is NP-complete and that if I add first-order quantifiers I get the complete problems for the polynomial hierarchy and PSPACE. What happens if my formulas are ...
- 2,204
0
votes
2
answers
67
views
Is there a model for the given logical formula, and if not, why?
I'm trying to determine whether there exists a model for the following logical formula: $(p_1 \to (p_2 \lor p_3)) \land(p_2 \to \neg p_3) \land ((p_1 \lor p_3) \to \neg p_2)$. Here's my understanding ...
- 3
4
votes
3
answers
701
views
What is practically preventing us from applying set-theoretic types in engineering?
I know the title is sort of misleading because we do have set-theoretic types in several languages:) From a theoretic view, set-theoretic types such as intersection, union, and negation may bring some ...
- 143