# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

980 questions
Filter by
Sorted by
Tagged with
1 vote
36 views

1 vote
58 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
32 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 ...
26 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 ...
167 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 ...
876 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. ...
32 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 ...
82 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
36 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$ ...
36 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 ...
286 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 ...
49 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 ...
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 ...
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 ...
1 vote
46 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'...
30 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 ...
42 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
30 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 ...
71 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 ...
31 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 "...
37 views

### Data structure for arithmetic logical queries

Abstract Problem I'm looking for a data structure that will (1) allow me to make queries of the form A.x - B.x <= 0.1 AND A.y + B.y >= C.y + D.y and (2) allow ...
22 views

### SOP Boolean expression of state variable and output of a Moore FSM

Disclaimer: I'm studying for an exam, but I don't have to hand in anything. I have the state transition diagram of the FSM and its states encoding: I want to find the sum-of-products (SOP) Boolean ...
1 vote
44 views

### Why do simple Logical Gates have an Irrational amount of Bits?

Suppose $2$ bits are used to encode a message, A and B. If you know $A$ is $1$, you have one bit of information. If you know $A\land B$ is $1$, you have two bits of information. If you know $A\land B$...
50 views

### Removing null production from cfg

While removing null production from cfg as below, S->ABC A->aA|^ B->bB|^ C->aaC|^ now as shown above we know that A,B and C all are ...
25 views

### Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$

I was reading "Open Logic book", "Sequent Calculus". Given the fact that all antecedents must hold for at least one succedent to hold, I can't get rid off the impression that using ...
78 views

### SAT polynomial time

Hi I understood it is not currently possible to solve SAT in polynomial time. Does this mean we can not currently solve an expression with n different boolean variables or with m different symbols in ...
51 views

### Is any 2-CNF has 2-DNF representation?

I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
49 views

### How to efficiently recalculate iterative weighted center

I'm trying to write a gradient ascent approach to divide all points on a polygon into two sets via a continuous line (something like the below, where our polygon is a circle and we partition such that ...
60 views

### Is finding a Polytime reduction from $L_1$ to $L_2$ equivalent to proving $L_2 \in P \Rightarrow L_1 \in P$

I often hear NP-completeness as problems such that, if they were in $P$ all problems in $NP$ are in $P$. The true definition, though, is that NP-complete is a set of languages in NP that all languages ...
59 views

### Proving that the polish notation has unique readability

I am familiar with the polish notation when it comes to algorithmically reading phrases, but I am having a hard time proving the following exercise: K is a function so that 1) $K(*)$ is an integer if ...
1 vote
57 views

### How do you deal with Skolem functions which escape their scope in elimination rules?

If you have an elimination rule for tuples which introduce the left and right pair into the type checking context, what do you do if the type of one of the elements is quantified and has been ...
1 vote
112 views

### How do you write a logic function to determine if one 2s complement binary number is less than another?

Working on logic design in class, and I'm trying to figure out how to write a specific logic function [and by write, I mean something along the lines of (x NOR y) OR (a NOR b), for example] It asks to ...
1 vote
59 views

### What is the Kripke semantic for a linear temporal logic?

I've read that in general for a modal formula P, a world w and a Kripke frame ⟨W,R⟩ w⊨□P if and only if for every u∈W, if wRu then u⊢P In case of LTL, being a modal logic, I assumed that the worlds ...
37 views

### How to make a GUI for first-order logic representation?

This idea blows my mind, I would appreciate for any guidance. In essence, the question is how a machine should work to transform any kind of formal logic into its graphical representation (e.g. ...
1 vote
48 views

### Application of a formal definition of $max, min$ to evaluate an expression

For an Algorithms course we are studying propositional calculus. As an excercise we are given formal statements which we are to explain in natural language first and then evaluate with specific values....
53 views

### What is the difference in heap configurations? Separation logic with CVC5 SMT solver

I am figuring out separation logic and trying to run simple examples in CVC5 smt solver. I am missing some core understanding of how pointers and values are treated there and I don't know where to ...
81 views

### Can we accept that all axioms are equivalent?

The proposirional logic is based on 3 schema of axioms of which (A1) is B ⇒ (C ⇒ B). Then, for any 2 axioms p and q, p ⇒ (q ⇒ p) is an instance axiom of (A1). We can have q ⇒ p by a step of MP as we ...
52 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 ... 1 vote
44 views

### Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$

Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ... 