Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
1 vote
2 answers
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 ...
3 votes
1 answer
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 ...
4 votes
0 answers
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 ...
4 votes
2 answers
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): ...
0 votes
0 answers
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 ...
-1 votes
0 answers
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
1 answer
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
0 answers
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: ...
0 votes
0 answers
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 ...
0 votes
0 answers
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 ...
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 ...
0 votes
0 answers
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(...
0 votes
2 answers
64 views

Aggregate text data of some particular column

I have a dataset as follows ...
4 votes
1 answer
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
0 answers
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
0 answers
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
1 answer
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
1 answer
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$ ...
2 votes
4 answers
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 ...
5 votes
2 answers
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, ...
2 votes
2 answers
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
2 answers
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
2 answers
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
0 answers
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 ...
0 votes
0 answers
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 ...
0 votes
2 answers
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,...
13 votes
1 answer
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 ...
0 votes
0 answers
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
2 answers
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
1 answer
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 ...
4 votes
3 answers
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
1 answer
45 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 \...
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 ...
1 vote
0 answers
25 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 ...
0 votes
1 answer
35 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 (\...
2 votes
1 answer
183 views

Natural deduction proof: distributivity of existential quantification

In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic: $(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,...
6 votes
2 answers
630 views

Is there an algorithm to detect race conditions in logic circuits?

I'm writing a logic gate simulator. I would like to prevent user from constructing circuits prone to race condition such as flip-flops, and instead provide them as separate building blocks. Is that ...
-1 votes
2 answers
87 views

Is there a quantifier more powerful than the other to determine FOL connector?

So basically we have 2 types of quantifier in first order logic, they are universal quantifier and existential quantifier. Usually we use implies connector(->) when we have universal quantifier in ...
0 votes
1 answer
53 views

How to find a term that proves a given proposition?

I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ...
0 votes
2 answers
51 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 ...
1 vote
1 answer
173 views

Are there any implementations of computability logic?

I'm currently looking into Japridze's computability logic. It looks great, but I was wondering whether any programming languages or systems implement it. Does anyone know of any implementation? ...
0 votes
2 answers
88 views

Z-Specification = Routes

Im trying to make an invariant for this Z schema about routes. 1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
6 votes
1 answer
709 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 ...
1 vote
2 answers
112 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=...
7 votes
1 answer
357 views

Direct conversion from regular expression to MSO

A language $L \subseteq \Sigma^*$ can be described by a regular expression iff it can be defined by a formula in monadic second order with words as structure $(\{0, \dots, n-1\}, <, (P_a)_{a \in \...
1 vote
0 answers
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 ...
3 votes
1 answer
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 ...
5 votes
4 answers
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. ...
0 votes
0 answers
28 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 ...
0 votes
0 answers
36 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 ...

1
2 3 4 5
20