Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
1 vote
1 answer
10 views

What is the proper way to write logic formula, say concerning graph theory?

Say for example I'd like to state that there exists a pair of vertices such that they form an edge in one graph but not some other graph. I'd go about it as follows: $$ \exists u, v \in V, (u,v) \in G,...
-3 votes
0 answers
15 views

Binary Sequence

Computer is used to control security lights given as 0110010. The system is programmed in that there will be light when 10101010 trigger switch is activated while switching signal is given as 01010. ...
0 votes
1 answer
57 views

Is "Bitwise Complement Operator" (~ tilde) distributive?

To be more precise, Is ~(a+b) = ~a + ~b? Here, "~" bitwise NOT operator. I ran into this question while thinking about ...
  • 1
0 votes
1 answer
30 views

Logic for Computer Science - How to define msort, merge and split functions inductively?

In "Modelling Computing Systems: Mathematics for Computer Science", I came across a logic exercise to inductively define a merge sort function 'mergeSort', with a hint to first define ...
0 votes
0 answers
19 views

Constrained Horn Clauses vs. "ordinary" Horn Clauses

I see why ordinary Horn clauses (of the type Prolog might accept) are first order eg something like (with all variables universally quantified) $$ P(x) \leftarrow Q_1(x),Q_2(x,y).\\ P(x) \leftarrow ...
  • 262
0 votes
0 answers
13 views

Converting regular expression to WS1S formula

Is there a "textbook" procedure to convert a regular expression such as $((0,1)(1,0))^*$ to a formula in WS1S?
  • 2,230
1 vote
1 answer
35 views

K in SKI combinator calculus: why doesn't it take one parameter since it ignores its second?

In the SKI combinator calculus, Kxy returns the constant function which always returns x. Since y is always ignored, why not just define K as having a single parameter, namely, x? What is the purpose ...
  • 159
2 votes
1 answer
45 views

Safety VS. Liveliness Property

I have to prove whether a certain property is safety or liveliness. The property represents the absence of deadlock so I expected it to be a safety property from what I read online. The issue is that ...
1 vote
0 answers
25 views

Relational calculus: "Find all X with at least y amount of Z"

Assuming I have two relations: Supplier [ID (PK), Name, City, Country] and Item [ID (PK), Name, Department, Price, Stock, Supplier_ID (FK)] What would be the easiest way to determine the following ...
  • 11
0 votes
1 answer
49 views

Using hypercomputation for "impossible" problems?

In mathematics and philosophy there are some unsolvable problems like Russell's paradox or the liar's paradox that are usually said to be undecidable... There are also other "impossibilities"...
  • 101
1 vote
1 answer
34 views

Proof that propositional resolution is refutation complete

I am studying theoretical computer science and I am in the part about resolution in propositional calculus. I was reading a theorem (and its proof) that propositional resolution is refutation complete,...
0 votes
0 answers
33 views

Complement of a language definition

Let $A=\{$ M is a TM, $s\in \mathbb{N}$ and $\exists x\in\Sigma^*$ s.t M rejects $x$ in at most $s$ steps $\}$. I want to define its complement, so how do I negate "$\exists x\in\Sigma^*$ s.t M ...
  • 21
-4 votes
2 answers
27 views

Let F be a function defined for all nonnegative integers by the following recursive definition

Let F be a function defined for all nonnegative integers by the following recursive definition. F(0) = 0, F(1)= 1 F(n + 2) = 2F(n) + F(n +1), n>0 Compute the first six values of F; that is, write ...
  • 1
0 votes
0 answers
20 views

Hoare Logic - Interpreting identity

I'm having some issues on understanding the following identity: { P } S { Q } ≡ [P ⇒ wp.S.Q] Does this means that if I have something like: ...
0 votes
0 answers
26 views

Minimum DNF length of a conjuction of equivalences

Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses. I am puzzled on what approach to take -- whether to ...
0 votes
2 answers
31 views

Logical equivalence priority

I have the logical formula $$ A \Leftrightarrow B \Leftrightarrow C $$ In order to make the truth table I'm not sure wheither I should interpret it as $A \Leftrightarrow B \Leftrightarrow C$ or $A \...
-1 votes
1 answer
58 views

Does quantum computing imply LPO?

The binary expansion of a given real number can be encoded as an amplitude using the inverse QPE. Together with Amplitude Amplification, I wonder if this could indicate that the (some weakened?) ...
1 vote
2 answers
44 views

"Largest set" in coinductive definitions

In several explanations of coinductive definitions (for example, in the answers to What is coinduction?), we're told that while an inductive definition gives us the smallest set with a specified set ...
  • 936
1 vote
0 answers
51 views

Method for simplifying complex logic tables

Not sure if this is the right StackExchange site, but back in college (20 years ago) I took a Digital Systems Design class where we learned how to reverse engineer a boolean function to meet the ...
0 votes
2 answers
37 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
30 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
186 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
37 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
58 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
28 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, ...
  • 109
1 vote
1 answer
59 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
78 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
145 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
50 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
33 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
45 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
41 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
102 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
86 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
116 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
108 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
38 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
36 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))$$
  • 121
1 vote
0 answers
33 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
40 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
194 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
46 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
28 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
25 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

1
2 3 4 5
19