Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
0 votes
2 answers
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 ...
0 votes
0 answers
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
7 answers
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
-2 votes
1 answer
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 ...
0 votes
1 answer
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 "...
1 vote
0 answers
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
1 answer
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 ...
0 votes
1 answer
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 "...
0 votes
0 answers
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 ...
2 votes
1 answer
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 ...
0 votes
1 answer
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
1 answer
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?
0 votes
0 answers
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 ...
0 votes
0 answers
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 \...
  • 1
0 votes
0 answers
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 ...
0 votes
0 answers
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 ...
0 votes
1 answer
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
0 votes
1 answer
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
2 answers
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 ...
14 votes
6 answers
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 ...
0 votes
1 answer
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
0 votes
0 answers
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
1 answer
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
1 answer
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
0 answers
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 ...
0 votes
1 answer
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
2 answers
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
1 answer
45 views

Why we can't use deduction theorem on soundness to contravene second incompleteness with lob's theorem

I'm starting to learn modal logic and there is something that's bothering my mind for a while. we know from deduction theorem that $((\vdash q) \rightarrow (\vdash p)) \Leftrightarrow(\vdash (q \...
1 vote
0 answers
26 views

What knowledge do players $y_1$ and $y_2$ have exactly in this example for Dependency Quantified Boolean Formula?

In [1], the authors give the following example to explain how Dependency Quantified Boolean Formulas (DQBF) work: As an example for a DQBF, consider the formula $∀x_1∀x_2∃y_1(x_1)∃y_2(x_2) : (x_1 ∧ ...
0 votes
0 answers
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
0 votes
0 answers
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,...
  • 1
0 votes
0 answers
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 ...
  • 1
2 votes
1 answer
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
0 answers
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
10 votes
4 answers
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,...
3 votes
1 answer
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
1 answer
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 ...
user avatar
0 votes
0 answers
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 ...
0 votes
2 answers
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 ...
0 votes
0 answers
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 ...
2 votes
0 answers
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
0 votes
0 answers
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
0 votes
0 answers
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 ...
0 votes
1 answer
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...
0 votes
0 answers
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 ...
3 votes
1 answer
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
-1 votes
1 answer
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 ...
2 votes
2 answers
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 ...
2 votes
1 answer
43 views

Resolution algorithm does not seem to generate the empty clause

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 ...
0 votes
0 answers
167 views

Construct CFG of monadic logic

How to construct CFG for tautologies in monadic predicate logic in the empty model. The predicates are Q and P, operations are ...

1
2 3 4 5
19