# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

1,016 questions
Filter by
Sorted by
Tagged with
31 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 vote
57 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
29 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 ...
28 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
47 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 ...
24 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
61 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$...
47 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
39 views

• 555
12 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, ...
39 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 ...
• 324
10 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
21 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
125 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
23 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
56 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 (...
103 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
609 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
37 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
33 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
73 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
36 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 ...
71 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 ...
28 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 ...
74 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
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 ...
49 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(...
• 195
196 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
52 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
36 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
58 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 ...
• 331
38 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
137 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
50 views

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 38 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 ... • 324 1 vote 2 answers 59 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 60 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 ... 4 votes 3 answers 684 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 ... 6 votes 1 answer 713 views ### Representing binary functions with a finite gate set without exponential blow-up? It is pretty well taught that any binary function can be represented using CNF. But conversion to CNF can take an exponential number of gates. The truth table is exponentially sized relative to the ... • 327 0 votes 1 answer 45 views ### How big is a formula equivalent to a wff over$n$variables with$2^n$subformulas? Definitions: Let$n \in \mathbb{N}$. If$\alpha$and$\beta$are propositional formulas, then we'll call$\alpha$and$\beta$independent if neither implies the other, or more formally, if$\lnot (\...
• 935
1 vote
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 ...