# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

925 questions
Filter by
Sorted by
Tagged with
28 views

### Boolean Logic when one component switches from 0 to 1

I recently was constructing boolean logic for all sorts of examples from Morris Mano's "Digital Logic and Circuit Design". I noticed that it is possible to construct a boolean logic wrt the ...
27 views

### Can you help me confirm this proof is valid for the Sequence Alignment lemma?

I'm reading the text Algorithm Design by Jon Kleinberg and Eva Tardos. In Chapter 6, the dynamic programming chapter, they discuss the Sequence Alignment algorithm and its importance to computational ...
1 vote
168 views

### How to design a faster sort algorithm? Is there sort of meta-algoritm for it? Or we do not understand how better sort algorithms were discovered?

I know that Quicksort or MergeSort are faster than, say, Bubblesort or Selection sort. And I know why (complexity metrics) but I never been able to find out how could someone start with, for example ...
• 113
32 views

### How to round numbers to its 0.5 superior in python

So basically my question is if i have for example 2.2 i need to create a python function to round numers to its higher 0.5 part, i mean 2.2 --> 2.5 2.3 --> 2.5 2.5 --> 2.5 2.6 --> 3 I cant ...
57 views

### What defines a byte?

I am asking this question because for some reason ascii codes from range 128 - 255 have a size of 2 bytes but their composition is 8 bits which makes them a "...
• 23
1 vote
22 views

### Are there systems in computer science where we have several logic systems working all at once and without isolation?

Are there systems in computer science where we have several logic systems working all at once and without isolation? I am thinking there are system where subsystem A uses Paraconsistent logic, ...
• 111
1 vote
45 views

### Simple Skolemization Question

Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
73 views

### If computers only work with intuitionistic/constructivist logic, so how it works with binary code?

Constructivist mathematics states that in order to prove something, we must construct this something, in a notion similar to computation, where things don't spring out of nowhere from some "...
35 views

### resolving in CDCL

When resolving in Conflict driven clause learning, it is the case that if you resolve a conflicting clause with the reason of the negation of one of his literals, then this results in another ...
125 views

### Formal language rewrite rules: strange notation

I'm reading "Program=Proof" by Samuel Mimram, and they use a notation for defining a formal language that I'm not familiar with. Here is how "Program=Proof" defines a formal ...
50 views

### Boolean Logic for Floats

I would like to know whether a theory exists which generalizes boolean logic to floats. Specifically, assume that instead of booleans 1 and 0, I have True/False tendencies, such as 0.9, where 0.1. ...
1 vote
38 views

### substitution of same variable in context-free grammars

Above is a theorem coming from the book "Formal languages and automata" by Peter Linz concerning substitution of variables. Could someone explain why A and B have to be different variables?
27 views

### Prove a Predicate is Primitive Recursive

Suppose $x$ is Godel's number of some formula. Predicate $\operatorname{P}(\operatorname{f}(x))$ is true only when the number of functions is equal to the number of predicates in that formula. Prove ...
41 views

### First-Order logic exercise

I'm trying to solve the following exercise: Given this is true: \begin{align} \neg \forall x \space \ \exists y \ ( x\neq y \rightarrow LeftOf(x,y) )\end{align} Demonstrate : \begin{align} \exists y \...
39 views

### Given a 2D Array (of 0's and 1's), find the minimum number of rows required so that maximum columns have their sum greater than a threshold

I have a 2D array of some rows and columns which are having only 0's and 1's. I would want to know if there is a way to optimize the number of rows so that maximum number of columns have their column ...
75 views

### Horn Satisfiability is NP Complete, isn't it?

To show that any formal language is NP Complete first it must be showed that this formal language is both in NP and NP Hard. So to show that Horn Satisfiability is NP Complete first it must be showed ...
84 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,...
• 11
51 views

### How can I prove that LTL formula is valid?

I do not know with which technique i can prove if a LTL forumula is valid. Let's say we have for example this one: ¬q U(¬p ∧ ¬q) → ¬Gp. How can prove if this valid or not? (should be true in any state ...
• 3
1 vote
92 views

### Combinational logic check if bits is prime

I wonder if there's Digital Logic Circuit (using combinatorial logic gates) that check if number is prime or not. For example given input fixed 8-bit that will produce 1-bit output. 00000101 will ...
5k views

### Is it provably true/false that for a program, there exists a proof whether it halts or not?

A standalone statement of my question Given a program that takes no argument, we are interested in whether the program will eventually terminate. My question is this: Theoretically speaking, can we ...
• 188
34 views

### Universal quantification and the number of solutions

How would one count the amount of solutions to quantified formulas that have universal quantifiers? For example, for a boolean formula $\Phi(X)$ with a number of solutions $\#\Phi(X)$ let's construct ...
• 1,393
32 views

### How to mathematically convert an array of bytes to a decimal value

With C# I can convert an array of bytes to a decimal value: ...
• 101
1 vote
20 views

### How to come up with combination a short-circuit evaluation table?

(a || b) || (c && d)) Given the above, how do I derive the table below: a b c d output T - - - TRUE F T - - TRUE F F T T TRUE F F T F FALSE F F F - FALSE I'm told that this is short ...
• 11
1 vote
39 views

### What does :: indicate in all-quantifier predicates?

Can somebody explain to me the meaning of $::$ in the following predicate? $$(\forall i : P(i) : Q(i)) \equiv (\forall i :: P(i) \implies Q(i))$$
• 117
1 vote
31 views

### Is it coherent to treat the C programming language as a formal system? [closed]

This is cross-posted from a similar question on Mathematics Stack Exchange, on the advice of a commenter. In mathematical logic, a formal system is a structure which includes, amongst other things, a ...
• 111
34 views

### How to converts Pseudo boolean constraints to cnf format?

How to convert Pseudo boolean constraints to CNF format for example L1 + … + Ln ≥ 1 is converted to L1 ∨ … ∨ Ln but how about: L1 + … + Ln ≥ k L1 + … + Ln < k or L1 + L2 = k or 2 L1 + 2 L2L3 + L4 ...
• 25
1 vote
192 views

### Logical consequence problem, doubt

It is possible to have this logical consequence? $$\forall x (p(x) \vee q(x)) \models \forall x p(x) \vee \forall x q(x)$$
• 13
1 vote
45 views

• 582
19 views

### Algorithm to Detect Disjunctive Relationships

I'm working with logic formulas of the form '0 & 2 | 0 & 3'. I was wondering if anyone knew of an algorithm that would take in such a formula, detect existing disjunctive relationships, and ...
• 1
23 views

### Creating a new list with with every other element

I am new to Isabelle, I am looking for a way to extract every other element of a list into a new list. Similarly, how do I extend it to extracting every 3rd element of a list? For example, given [1,2,...
19 views

### How to specify in Isabelle that there exists j in an interval

I am looking to specify something in Isabelle of the form that there exists a $j$ such that $lb < j < ub$, where $lb$ and $ub$ are lower and upper bounds. For a single condition, we can say, for ...
58 views

### Is $f(X)f^d(X) = 0$ for a Boolean function $f$?

I'm currently trying to understand a step in the proof for in the Crama and Hammer book on Boolean Functions. The proof is Proposition 4.12, which claims that the self-dualization of Boolean $f$ is ...
• 419
1 vote
28 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 ...
• 131
5k views

### Could Gödel’s incompleteness theorem be circumvented with a quine?

As you all probably know, Gödel’s incompleteness theorem states, that it will never be possible for mathematics to prove its own correctness. Mainly because that proof would be part of mathematics too,...
• 225
134 views

### Building non-classical logics in Agda & Coq

Is it possible to construct different systems of logic in Coq or Agda? I ask because I'm interested in using a proof assistant to construct (and verify) theorems in things like many-valued logics, ...
1 vote
115 views

### Proving a predicate assignment is correct

I am currently reading Formal Methods - An Appetizer and am stuck in chapter 3 (Program Verification). I am unfamiliar with logic and I do not think I understand the $\vDash$ notation correctly. I ... 72 views

### Logic Gates - 3 Sensors in a Factory

I am studying logic gates and I encountered this problem: A set of three sensors in a factory detects whether the pollution level it is outputting from an incinerator exceeds the safety limit. In ...
• 111
69 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 ...
66 views

### Set, then get, or first get, then set?

In some abstract programming languages there is a concept "setter and getter". Generalizing, should this be the opposite, i.e. "Getter and setter"? I would theorize that one should ...
39 views

### Reading list for mathematics and formal logic with missing truth values?

I would like a reading list of math and formal logic books which give a principled discussion of missing values. Textbooks on mathematics and formal logic - propositional and first-order and higher-...
• 163
30 views

### Is there an efficient way to generate a pseudo-boolean function from a linear constraint?

I would like to define a pseudo-boolean function $f$ such that $f(x) = 0$ for all logically valid combinations of $x\in{0,1}$ and $f(x) > 0$ for all logically invalid combinations of $x\in{0,1}$. ...
• 121
25 views

### how would i go about creating a base 10 to base 2 converter

I am trying to create a calculator in excel for use in Minecraft later and I was wondering if the was any way to create and how I would create a base 10 to base 2 converter with only logic gates. if ...
38 views

### How do logical and bitwise operators work on numbers? (e.g "2 and not 5")

====TLDR============================================================= Curious about the behaviour of logical and bitwise logical operations on integers, i.e with and...
179 views

### 8-bit binary to bcd converter Verilog

We have been given task to write a 8-bit binary to bcd converter Verilog code, using structural code NOT behavioural, is it possible to guide us how can we create 8-bit binary to bcd converter using ...
46 views

### Stalmarck's method: x ≡ x → z, does z have to be true?

I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that: y $\to$ z $\equiv$ x where x, y and z are booleans which ...
• 53
31 views

### Conjuctive Normal Form

Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if Q and R have different truth-values; or P and R have the same truth-values. Choose all formulas that are in conjunctive ...
103 views

### What if solving P vs NP revealed a contradiction?

Let's just say that some person discovered that $P = NP$ implies $P \neq NP$ and $P \neq NP$ implies $P = NP$, and we don't know what is causing this contradiction, And this was a valid proof that was ...
Let's assume I have the following 3 clauses: $\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$ and I want to see if our KB entails $\neg U$ so I tried to apply ...