# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

1,001 questions
Filter by
Sorted by
Tagged with
45 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 ...
• 121
11 views

### How to extract Geo880 and Jobs640 dataset? [closed]

The links to both datasets are below: https://www.cs.utexas.edu/~ml/nldata/jobquery.html https://www.cs.utexas.edu/users/ml/nldata/geoquery.html I attempted to download them via FTP, but I can't ...
590 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
32 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
33 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
25 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
59 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 ...
1 vote
33 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 ...
70 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 ...
27 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 ...
1 vote
59 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: ...
• 193
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 ...
43 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 ...
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 ...
15 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(...
• 181
191 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 ...
• 203
1 vote
50 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
34 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
1 vote
52 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 ...
• 321
30 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
113 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
28 views

### Karp-reduction of Disk Covering Problem

While preparing for final exam, I encountered a (target) problem where you have $M$ lines and $L$ points and you want to answer if it's possible to cover them all using $K$ disks of unit radius (...
• 115
1 vote
45 views

• 925
1 vote
71 views

### DFA for even concatenation of strings from a language

If I have a deterministic finite automaton (DFA) with a language $W$, and I need to create another DFA that returns all the strings that are a concatenation of an even number of strings in $W$, how ...
1 vote
36 views

### How to prove a minimum number of queries needed to determine a piece of information

You have 27 coins, 1 of which is a different weight. Using a balance scale with 2 pans, how can you determine which coin is different in only 4 weighings? Generalize this to N coins. Hint Solution ...
• 145
29 views

### Prove with natural deduction

Prove P ∨ Q, Q ∨ R, P → ¬R |- Q with natural deduction. P ∨ Q, premiss Q ∨ R, premiss P → ¬R, premiss ... ... Conclusion, Q I dont know how to properly solve this question? I know somewhat how to ...
170 views

### how to do incremental construction of the minimal model in logic programming?

I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the ...
• 1,004
958 views

### Curry-Howard isomorphism and non-constructive logic

My understanding of the Curry–Howard correspondence is that it shows an isomorphism between constructive logic (also called intuitionistic logic) and computer programs in appropriate typed languages. ...
• 231
37 views

### Growth of a set of propositional formulas under partial evaluation

Definitions: Let $n \in \mathbb{N}, n \geq 1$. We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic. We define partial evaluation in the normal way ...
• 925
85 views

### Is there a 2SAT encoding for a NAND gate

I am trying to encode some circuit checking algorithms, but encountered difficulty creating a 2SAT representation for a NAND circuit. Is there a proof that this is not possible?
1 vote
39 views

### Complexity of a Set of Formulas

Notation: We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic. Consider an expression $\alpha_n$ in disjunctive normal form built from $2n$ ...
• 925
48 views

### Are recursive Horn clauses first order?

My understanding is that recursive definitions are considered second-order since they require the fixpoint operator in order to be formulated as "true" definitions. This is even though they ...
• 282
323 views

### Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?

If I understand correctly, the first incompleteness theorem says that any "effectively axiomatized" formal system which is consistent must contain theorems which are independent of the ...
53 views

### Could there be a computer or components based on a non-classical logic?

Since circuits and processors are heavily influenced and designed based upon boolean logic, which is itself a subset of propositional logic, could there be different interpretations of hardware or ...
• 103
33 views

### Given a population, find the boolean algebra expressions that most closely evaluate to that population

TL;DR I have some ideas but am curious to know if there are existing proofs, research, etc. in this area that I can use to guide my algorithm development. Problem summary We have a population where ...
• 101
27 views

### Equivalent logical statements confusion

First time posting here. If we have the logical statement ($A$ and $B$) $\rightarrow$ $C$ ($1$), we know that it is equivalent to ($A$ and $B$) $\rightarrow$ ($C$ and $A$) ($2$). Therefore if we ...
• 101
63 views

### How to express that a graph has Independent set of size at least $n/2$ in $\exists SO$

I am looking to provide a formula saying "A graph with $n$ vertices has an independent set $X$ of size at least $n/2$" in existentional second order logic. (This is exercise 1.2. from Libkin'...
35 views

### Worst Case Response Time (WCRT) analysis the only necessary test for real time tasks?

Recently, I have taken a Computer Science exam for the course Operating Systems. One question was as follows: Which statements about real-time operating systems are true? I selected two options, but ...
53 views

### Defining 2 inductive propositions relying on each other in Coq

I'm pretty beginner in Coq. I want to formalize negative and positive occurrence of an atom in a proposition inside coq the definition is as down below: I want to define this property as an Inductive ...
1 vote
36 views

### Shortest unsatisfiable 3-CNF that can't be refuted with narrow resolution?

Proof width (the size of the largest clause in a proof) plays an important part in refuting an unsatisfiable formula. If a formula has a bounded-width resolution proof of its unsatisfiability, then ...
• 25
97 views

### Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic

Intuitionistic logic(s) are usually defined in a purely synthetic way, with their own deduction rules different from classical logic, but they also have semantic interpretations. One of them, more ...
• 131
39 views

### What are the applications of Belief Revision?

In my Computer Science graduation, I came across this concept of Belief Revision, which focus on knowledge representation and the possible operations that can be done with the facts that a "...
• 103