# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

869 questions
Filter by
Sorted by
Tagged with
9 views

### Frequency of electric impulses from keyboard input into computer? [closed]

What is the frequency of binary code (example on graph :1010101) from keyboard input for computer to read? Is there a specific computer frequency that is high or can I just use low frequency to input ...
26 views

### "Universe-shrinking" function in Agda

Agda does not allow datatypes in one universe to be indexed by, or non-trivially parametrized by a type in a larger universe (strangely, Coq does not appear to require this for propositional ...
60 views

### To prove (KB ⊭ S) and (KB ⊭ ¬S) is satisfiable

In question (e), I have to prove: A ≡ (KB ⊭ S) and (KB ⊭ ¬S) is satisfiable, where KB and S are propositional variables. I am not able to follow the solution given in the image above as to why it is ...
82 views

### XOR gate from default-on/default-off relays, this simplest possible?

Playing nandgate to learn logical gates. Is the design below the simplest xor gate that can be built using the relays available? Seems like crossover relays allow a much simpler xor gate but don't ...
90 views

### Satisfiable CNFs where each clause contains logarithmically many different literals

Studying for my finals in Complexity theory. This question comes up in different variants and it requires to use probability. A side note before, to be more clear: A CNF clause consists of $n$ clauses ...
100 views

### Why is it useful to transform 0-1 integer programming problem into SAT problem?

There are several researches studying translating 0-1 integer programming into CNF form. For example, this paper and this C++ library. As the lecture notes here goes, translating 0-1 integer ...
36 views

### Is there an alogrithm that analyses mistakes and increses weighting of a certain subject based on the mistake?

I am building a program that analyses a students mistakes and that mistake is linked to a topic. Then the program gets the information that a certain person has made x mistakes on some topic. I want ...
59 views

### Incomplete definition of function- first order logic

Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations. Let $\Sigma_2=\{c,g^2,R_1^1,...,R_k^1\}$ where $c$ is constant, $g$ is two ...
90 views

### Problem with formalism in first order logic

This is a general question in first order logic. Assume I have alphabet $\Sigma$ that contains one-argument function (among other symbols). I want a new alphabet, $\Sigma'$, which is the same as the ...
58 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 ...
38 views

### Herbrand universe with infinite terms (for a lazy programing language)

I am working with a toy programming language for my thesis. It is lazy evaluating so I can have infinite terms (for example the "infinite natural number" ...
64 views

### Proving that there are more problems than solutions

I have doubts regarding a proof of the following theorem: 'Set of all problems' is larger than the 'set of all algorithms' (or set of all C programs). Put rhetorically, the theorem says that there are ...
37 views

### What are the limits of Boolean Algebra?

Any decision problem algorithm can be represented as a boolean expression. The rules of boolean algebra (De Morgan's law, distributivity, etc.) can be used to manipulate and simplify that expression, ...
30 views

### Is an AND gate which is noisy 1/3 of the time on only one of its inputs universal?

Imagine you have a noise-free NOT gate, and an AND gate with the usual truth table 00 0 01 0 10 0 (*) 11 1 but such that the case (*) is wrong 1/3 of the time, ...
29 views

### What Is the Currently-Known Simplest NOR-node Directed Cyclic Graph That Produces Pi?

Any directed graph (including a directed cyclic graph or DCG) has a complexity measure. We know that NOR is a universal logic gate, in the sense that a DCG whose nodes are n-input NOR gates can ...
43 views

### What is meant by A determine BC in functional dependency. How the validity of this statement will be checked

We use notation A determines BC in a database for functional dependency. Same way we use equations in mathematics which shows dependency of variables. We have inference rules in logics, functions in ...
21 views

### Software for proving tautology with steps

I'm looking for a software which can prove a tautology using logical equivalences. It should be able to show each step. So you can follow the chain of reasoning. Here is an example: \begin{align} (p\...
248 views

### Weird "proof" recursion

Assume we have some statement called $\alpha$. We will define a new statement $P(\alpha):="(\alpha\text{ can be proved})\lor(\lnot\alpha \text{ can be proved})"$ I claim that $P(P(\alpha))$ is always ...
35 views

### Is a Turing Machine a Well-formed formula?

Today i wrote something about the bijection between turing machines and recursive functions. And i describe a Turing Machine as a Well-formed formula because it seems like a WFF to me. But is it ...
45 views

### Proving intuitionistic tautologies in Agda

I am to use Agda to prove some intuitionistic tautologies. One of them is the so called Weak Peirce's Law $$((((A \rightarrow B) \rightarrow A) \rightarrow A) \rightarrow B) \rightarrow B$$ I ...
38 views

### What is the connection between finite automata and logic (sequential calculus)?

Languages recognized by finite automata are exactly those definable by sentences of the sequential calculus, and also exactly those definable by rational expressions (also called regular expressions) ...
38 views

### a conjunctive normal form that is a tautology

Are there any examples of CNF formulas that are tautologies? Such that every clause contains different variables so phrases like (a or not a) are rejected?
34 views

Using the Fitch application and only Intro and Elim rules (& REIT if necessary), prove that $$\forall x \forall y (P(x) \implies Q(y)) \iff (\exists x P(x) \implies \forall y Q(y))$$ is a logical ...
18 views

### Analogue of disjunction and existence properties for a Turing-complete programming language?

Quoting from Wikipedia: In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories ...
21 views

### Hoare Triple Logic

I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X} ...
22 views

### Are single complements the same as seperate complements?

Is (A' + B') the same as (A + B)' ? Note: The apostrophe ( ' ) represents the complement
31 views

### Complexity of pattern matching for modus ponens logical conclusions

Is a Turing machine with added the following contant-time operation equivalent (in the sense that polynomial time remains polynomial time and exponential time remains exponential time) to a (usual) ...
16 views

49 views

### Can anyone explain the pigeon-hole encoding method in proportional logic

Someone there who worked with cardinal contraindications within the framework of propositional logic? I have a problem understanding the pigeon-hole method. It is a method of satisfaction. I have been ...
24 views

### Doubt regarding the implications of a 2-SAT constraint

Consider an example 2-SAT instance with the constraint (x1​ ∨ x2)​. This CNF has these two implications: ¬x1​→x2​ and ¬x2​→x1​. "They actually mean, if x1​ is false then x2​ must be true, and if ...
20 views

### Newbie 2s complement to binary circuits help

I'm creating a circuit with in3, in2, in1, and in0, and outputs F11-F0. The circuit has to take the input in 2s complement and output the number in binary with the sign. F11 represents the sign bit (...
29 views

### Formal Logic - Natural deduction: Problem with assumptions about exists-negation

I'm stuck on how to progress with this proof, despite I have tried, I cannot see the next move. Given this proof without predicate: So far what I've accomplished: My idea is, as I can't see any ...
13 views

### Good exposition of tableau for first-order logic with equality?

I'm looking for a resource (online or printed) that explains in a self-contained way the classic tableau for first-order logic with equality. All I can find are expositions of tableaux for first-order ...
154 views

### Number of substrings possible with even characters

Consider a string 'ABBAA' Possible substrings with even number of characters are $4$ 'ABBA' : Count of 'A' is even and 'B' is even 'AA' : Count of 'A' is even and 'B' is even - ($0$) Similarly 'BB' ...
160 views

### How do computers *really* work? (at the most basic level)

While learning about computers I will read about RAM and Storage and the CPU, and while these explain the architecture of a computer and how parts of a computer work together, I still don't understand ...
18 views

### Proving using a SAT solver that KB entails D

Suppose you're given this KB: $$KB = (A, A ⇒ B, A ⇒ C, B ∧ C ⇒ D)$$ How would you show using a SAT solver that $KB \vDash D$?
47 views

### Oracle that can only definitively say if an instance is unsatisfiable

Assuming I have an Oracle that takes as input a strictly 3SAT Boolean instance and states whether the instance is satisfiable or not. If it says instance is unsatisfiable then the instance is ...
50 views

### Number of substrings with exactly k distinct characters

Given a string s and an int k, return an int representing the number of substrings (not unique) of s with exactly k distinct characters. If the given string doesn't have k distinct characters, return ...
27 views

### Showing that a bijection preserves homomorphism

I have the vocabulary $\tau = \{+, 0 \}$ and the structure $R = (\mathbb{R}, +^R, 0^R)$ where $+^R$ is a binary function symbol representing the normal addition of numbers and $0^R$ is the constant $0$...
189 views

### Encoding the theorem on friends and strangers in predicate logic

In every group chat of six (distinct) people on Instagram, there is a group of three (distinct) people such that either: everyone in the group are friends everyone in the group are strangers (i.e not ...
27 views

### CTL and the modal mu-calculus

Is there any literature / results to which fragment of the modal mu-calculus the logic CTL corresponds? I know that in order to tranlsate the until operators of CTL, it suffices to use a single mu-...
29 views

### Converting into CNF

I am still a bit confused by how to convert into CNF even though I have the rules written down. How do I convert the following sentence into CNF? $(I \lor M) \Rightarrow H$ I know I need to get rid of ...
30 views

### Multiple parameter predicates and the Relational Model

I've got a very general question about the relational model and it's relationship to 1st order predicate calculus. It will probably seem very basic to most, I'm afraid, a consequence of me grappling ...
39 views

### Propositional Logic: Entailment

Given the sentences, S1, S2, if S1 |= S2 then all models that satisfy S1 also satisfy S2, how is the following statement correct? A ∧ ¬A |= B How can something and ...
49 views

### In propositional logic how is the negation equivalent?

I am unable to understand how the negation of a sentence into CNF actually makes sense, hopefully somebody can explain it to me in understandable terms! Given the sentence: If the battery is charged (...