Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

997 questions
Filter by
Sorted by
Tagged with
1 vote
29 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 ...
86 views

equivalence of validity above different alphabet

Given the next alphabets: $\,\,\Sigma_1=\{R^2,P^1,=^2\}\,\,,\Sigma_2=\{c,f^1,=^2\}.$ Prove of Disprove: There's exists an algorithm, that given formula $A$ above $\Sigma_2$, builds formula $A'$ above ...
66 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 ...
2k views

Do Karnaugh maps yield the simplest solution possible?

I'm learning to use a Karnaugh map, but I'm not sure if I obtained the simplest expression possible. Have a look at this example: Truth table (inputs are A B C; output is F): ...
26 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 ...
27 views

Logic circuit for complex boolean expression

Can someone help me with the solution of this boolean expression in a circuit: (A′B′CD′) + (A′BCD) + (AB′CD′) + (ABCD′) I was told that the output goes high only when all 4 inputs are high but I'm ...
1 vote
244 views

Translating Natural Language to LTL Formulae

I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct. I'm given the sentences, and my assumption is that $l$ ...
1 vote
52 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: ...
44 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 ...
39 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 ...
14 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(...
64 views

Aggregate text data of some particular column

I have a dataset as follows ...
186 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 ...
1 vote
47 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
25 views

About introducing a family of types into a type theory with inference rules

Suppose I want to introduce a new family of types $B(a)$, where $a:A$ into a type theory using inference rules. First of all, my understanding is that $B:A\to U$, where $U$ is some universe. So my ...
1 vote
97 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 ...
1 vote
251 views

Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite

I'm kind of desperate at this point about this question. A predicate-logic resolution derivation of a clause $C$ from a set of clauses $F$ is a sequence of clauses $C_1,\dots,C_m$, with $C_m = C$ ...
3k views

Resolution and what it means to derive the empty set

When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable? If this is the case, why is ...
384 views

propositional Modal logic filtration definition

Hello I have a slightly unusual question which relates to a definition of filtration structure. The following is my current state of the definition: $\mathcal{M} = (W, R, L)$, W is a set of worlds, ...
130 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 ...
1 vote
45 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 ...
1 vote
907 views

3 bit binary multiplier?

I have the following 2-bit binary multiplier (source: wikimedia.org) How can I modify this 2-bit binary multiplier to make it a 3-bit binary multiplier? I notice that there are 2 half-adders, and ...
1 vote
30 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 ...
29 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 ...
112 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,...
801 views

The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
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 (...
1 vote
273 views

Create a Deterministic Finite Automaton 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 ...
1 vote
69 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 ...
662 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 ...
1 vote
45 views

183 views

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 ...
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 ...
929 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. ...
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 ...