Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
0 votes
0 answers
30 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 ...
user avatar
2 votes
1 answer
115 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 ...
user avatar
0 votes
1 answer
46 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. ...
user avatar
1 vote
1 answer
36 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?
user avatar
0 votes
0 answers
19 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 ...
user avatar
0 votes
0 answers
36 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 \...
user avatar
  • 1
-4 votes
0 answers
72 views

2-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 2-Satisfiability is NP Complete first it must be showed ...
user avatar
0 votes
0 answers
37 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 ...
user avatar
0 votes
0 answers
62 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 ...
user avatar
0 votes
2 answers
71 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,...
user avatar
0 votes
1 answer
42 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 ...
user avatar
  • 3
1 vote
2 answers
82 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 ...
user avatar
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 ...
user avatar
0 votes
1 answer
33 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 ...
user avatar
  • 1,381
0 votes
0 answers
28 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: ...
user avatar
  • 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 ...
user avatar
  • 11
1 vote
1 answer
38 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))$$
user avatar
  • 115
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 ...
user avatar
0 votes
1 answer
23 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 ...
user avatar
  • 25
1 vote
2 answers
190 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) $$
user avatar
  • 13
1 vote
1 answer
40 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 \...
user avatar
1 vote
0 answers
24 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 ∧ ...
user avatar
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 ...
user avatar
  • 1
0 votes
0 answers
21 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,...
user avatar
  • 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 ...
user avatar
  • 1
2 votes
1 answer
56 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 ...
user avatar
  • 419
1 vote
0 answers
27 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 ...
user avatar
  • 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,...
user avatar
3 votes
1 answer
125 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, ...
user avatar
1 vote
1 answer
114 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
43 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 ...
user avatar
0 votes
2 answers
64 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 ...
user avatar
0 votes
0 answers
53 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 ...
user avatar
2 votes
0 answers
37 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-...
user avatar
  • 163
0 votes
0 answers
28 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}$. ...
user avatar
  • 121
0 votes
0 answers
23 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 ...
user avatar
0 votes
1 answer
35 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...
user avatar
0 votes
0 answers
141 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 ...
user avatar
3 votes
1 answer
43 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 ...
user avatar
  • 53
-1 votes
1 answer
27 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 ...
user avatar
2 votes
2 answers
101 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 ...
user avatar
2 votes
1 answer
42 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 ...
user avatar
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 ...
user avatar
3 votes
1 answer
49 views

CTL trouble translating text into formula

I have an excercise where I have to translate verbally formulated statements into CTL formulas. I have particularly trouble with this one: On every path q is true at least once and p was true ...
user avatar
  • 135
1 vote
0 answers
17 views

Proving set of register machines that halt before k steps for some input is non-recursive

Given an enumeration of register machines $R_n$ that take a single natural number as input, and a constant $k$, the function $f$ is defined as: $$ f(n) = \begin{cases} 1 & \exists m \text{ such ...
user avatar
  • 11
0 votes
0 answers
29 views

Specific quantifier elimination for real algebraic numbers

It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
user avatar
  • 113
3 votes
3 answers
152 views

How many possible arithmetic operations are there between two N-bit numbers?

It's generally considered to be the case that there are sixteen possible logical operations between two N-bit numbers and four possible logical operations on one N-bit number. I'd like to know how ...
user avatar
  • 81
1 vote
1 answer
66 views

Translating Natural Language to LTL Formulae

I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct. I'm given the sentences, and my assumption is that $l$ ...
user avatar
0 votes
1 answer
53 views

Domain of discourse vs First-order theory

In the question (Validity of predicate logic formulas) I see the following way of expressing: "The predicate $P(x,y) \equiv \bigl[ y \cdot x = 1 \bigr]$, where the domain of discourse is $\...
user avatar
  • 113
0 votes
1 answer
23 views

Determine if the following arithmetics are sentences

How would you determine if these arithmetics are sentences or not? -(x + 2) > y i++ == 2 i++ == 2 is this sentence True where i = 1 I understand it as if the ...
user avatar

1
2 3 4 5
19