Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
0
votes
0answers
23 views

A necessary condition for a relation to be in 2NF but not in 3NF is that some non-prime attribute must be determined by a non-prime attribute

I will state the complete question now, since it did not fit in the title. Is the statement given below correct? A necessary condition for a relation to be in 2NF but not in 3NF is that some non-...
0
votes
1answer
5k views

Finding weakest precondition

I have the following program x := y + 1; if (y > 0) then x := x + y else x := y + 100; x := x + y; I want to compute the weakest precondition for getting <...
3
votes
1answer
50 views

What's the average number of transistor switches needed to do an N-bit x N-bit multiply?

I want to know how switch-efficient a multiplier can be. If I need to do many $N$-bit by $N$-bit multiplies, and each bit is determined by flipping a coin, what's the average number of transistor ...
2
votes
0answers
34 views

Is there a diagram of related logics?

Proving software is based on logics and there any many logics. AFAIK all of the logics can be shown as a tree diagram of how they are related; for example, a tree of how types of number are releated ...
-4
votes
0answers
27 views

Prisoner's dilemna [closed]

b.Suppose a prisoner's dilemma game is defined using the following pay-off matrix. Table below: Use the table to help answer the ...
0
votes
1answer
38 views
5
votes
2answers
231 views

propositional Modal logic filtration definition

Hello I have a slightly unusual question which relates to a definition of filtration structure. The following is my current state of the definition: $ \mathcal{M} = (W, R, L) $, W is a set of worlds, ...
3
votes
1answer
40 views

Proving equivalence of two substitutions by induction

I'm trying to prove the following reduction: $$ t\{x:=u\}\{y:=v\} = t\{y:=v\}\{x:=u\{y:=v\}\} $$ under the following assumptions: $x \neq y$ $x$ is not a free variable of $v$ (in symbols, $x \...
-2
votes
2answers
72 views

How to correctly negate a predicate bounded by some quantifiers?

this is a problem which was asked in GATE CS 2010. This is question statement: Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
2
votes
1answer
26 views

Clarifying the definition of reduction with regards to NP-complete problems

In my logic class we started learning about the different complexity classes. In particular, we focused on the NP complexity class. A problem is in NP if it is solvable in polynomial time using a ...
4
votes
0answers
74 views

Understanding a paper on polynomial recursion in all finite types

So I wasn't sure weather or not this counted as "research level" or not but I figured it wasn't so I decided to post it here. There is a paper by S. Bellantoni et al. called "Higher ...
0
votes
1answer
98 views

Boolean expression for sum bit of full adder

The Boolean expression I find on the internet for the sum bit of a full adder is A xor B xor Cin. Does't this expression exclude the A=1,B=1,Cin=1 situation? When that happens, the sum bit is also 1, ...
2
votes
0answers
335 views

Prove that PRE-WORK-POST is Turing Complete

This is a homework question and I am trying to fully understand what I have to do and how to go about it. Therefore, I don't want full answers to the question. The programming language PRE-WORK-POST ...
0
votes
0answers
48 views

Is there any use in bivalent variables in computer science?

Is there any use in bivalent variables in computer science? By bivalent variable, I mean any variable that has 2 values at the same time as in: x = 2 and x = 4 x has both the values of 2 and 4 at the ...
5
votes
0answers
34 views

Do FOL theorem provers accept axiom schemata?

Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata? I looked in the Vampire "manual" briefly,...
0
votes
1answer
23 views

Which of these properties hold for all FO theories? (but not regarding fragments thereof)

Which of these properties hold for all FO theories? (but not regarding fragments thereof) a. Decidable b. At least expressive as propositional logic c. NP-complete a) Decidable: no, some first order ...
-2
votes
1answer
14 views

Consider 4 positive integers a,b,c,d having exactly 10^11 bits (considering the leading zeroes) in the binary representations

Consider 4 positive integers a,b,c,d having exactly 10^11 bits (considering the leading zeroes) in the binary representations. Positions are numbered from 1 to 10^11. Every 3rd bit of a is equal to 1 ...
0
votes
2answers
60 views

A basic question about predicate logic

Suppose we have a statement: "Tom has a car" and we have an auxiliary clause that is has(x, y): x has y then to write the statement in logic I am guessing ...
0
votes
0answers
20 views

Comparing Registers with 16-bits

I am given with this information: "CMP OP1,OP2 will compare registers OP1 and OP2 if they are equal, flag values will be ZF=1, CF=0, if the first operands value is greater flag values will be ZF=...
12
votes
1answer
540 views

The difference between dynamic logic and temporal logic

To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia: another variant of modal logic sharing many common features with dynamic logic, differs from ...
0
votes
1answer
31 views

Create an Finite Deterministic Automata for a regular expression

I want to create a finite state machine that accepts the following language: $$ L=\{w\in\{a,b\}^* | w \text{ contains abb but not on the first position}\} $$ So I began by writing a regular expression ...
0
votes
1answer
47 views

Consistent theory based on L and not(A->A) is a theorem

I am working on this problem in which I have a theory $T$ based on language $\mathcal{L}$ and the only information we have is that T is consistent and $\vdash \lnot(A \rightarrow A)$. Given this ...
0
votes
1answer
36 views

An equivalent of $\neg ((a \wedge b) \Leftrightarrow c)$ based on a specific requirement

I am solving a problem that is asking to provide an equivalent for $\neg ((a \wedge b) \Leftrightarrow c)$ and the equivalent shouldn't contain $\wedge$ (and), $\Rightarrow$ (implication) or $\...
0
votes
1answer
40 views

Is Conjunctive Normal Form or not?

I have one formula that I do not understand why it is CNF and one that is not CNF, namely. p && !q (NOT NCF) and !!p(CNF). According to the exercise where I found these examples, 1 is not ...
1
vote
1answer
84 views

Meaning of $a\lor b \to b' \lor c'$

So I have done part a) but I have no clue what I am supposed to do for part b), I have been trying for days to wrap my head around and even asked my fellow course mates, none of which seem to know ...
0
votes
0answers
41 views

What is the difference between type theory and logic programming (in terms of declarative programming and specification)

How is does type theory (coq, lean, agda), and logic programming (prolog, datalog) differ from each other. Logic programming is a way of declarative specifying an algorithm, using classical 1st order ...
4
votes
2answers
1k views

Turing-completeness, Conway's Game of Life and Logical Gates

I was recently given an assignment at university asking me to discuss the universal computational capability of Conway's Game of Life. I'm not required to actually build up a Universal Turing machine ...
3
votes
3answers
570 views

Does exist any horn formula that is equisatisfiable to the clause that is disjunction of two literals? Does also exist equivalent?

I just and simply want to know if whether or not exist any horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to know if there also exists equivalent.
2
votes
1answer
64 views

Natural deduction proof: distributivity of existential quantification

In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic: $(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,...
0
votes
1answer
32 views

is duality principle in boolean algebra is true for every expression

Let say A = 1 and B = 1 and then A+B = 1 now by using duality(replacing or gate by and gate and 1 by 0) we can say that, A.B = 0 but this is not 0, because 1.1 = 1, so please anyone clear my ...
0
votes
0answers
19 views

Is my UML Use Case Diagram valid?

I'm preparing an UML use case diagram for my following school project: ...
1
vote
0answers
34 views

Help me understand whether these critical pairs are joinable

I have the following TRS $R$: $$ l_1 = f(g(x)) \to f(x) = r_1 \\ l_2 = g(f(y)) \to g(y) = r_2 $$ I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$. I have ...
1
vote
0answers
50 views

Why is most research in logic and verification conducted in Europe rather than the US?

This is the CSRankings output for logic and formal verification for the last 10 years, worldwide: http://csrankings.org/#/index?log&world For the International Conference on Computer Aided ...
0
votes
0answers
12 views

How to combine multiple Boolean Functions in CDNF efficiently for implementation on a CPU?

I am trying to see how fast I can implement a 6-bits to 6-bites lookup table. Generally, I am attempting to do this by using the common method mentioned in CS textbooks of using the Quine-McCluskey ...
0
votes
0answers
20 views

Prove the boolean function E = F + G contains of the sum of the minterms of F and G

I'm given a boolean function E which is result of the sum of F and G (Where both F and G are boolean functions for sure). By using K-Map I can easily understand why E would have the sum of the ...
2
votes
0answers
22 views

Automated algorithm design

There is a huge field of study dedicated to automated theorem proving. Is there any similar research dedicated to automated algorithm design? And is there any form of "duality" between these ...
4
votes
2answers
16k views

The difference between a sequence and a set

I am new to discrete mathematics and the theory of computation I am trying to learn and understand the terminology. I am having a difficult time understanding the difference between a set and a ...
2
votes
0answers
33 views

Name for a function on formulae that does not break the structure of given formula

I have two logics, $L_1$ and $L_2$, and a mapping $f: Formulas_{L1} \rightarrow Formulas_{L2}$, and want to argue that the mapping is "nice", in the sense that it is structure-preserving. ...
1
vote
1answer
40 views

Z-Specification = Routes

Im trying to make an invariant for this Z schema about routes. 1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
1
vote
0answers
32 views

Check if given safety properties are regular, and if so construct NFAs

Let $\mathit{AP} = \{a, b, c\}$. Consider the following LT properties: Between two neighboring occurrences of $a$, $b$ always holds. Between two neighboring occurrences of $a$, $b$ occurs more often ...
4
votes
0answers
195 views

Can every sentence of first-order logic be converted into an equisatisfiable equation in Boolean algebra?

There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational ...
5
votes
1answer
97 views

proving program equivalence

I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
3
votes
2answers
85 views

How expensive is it to verify that a gate is universal?

I know that a NAND gate is considered universal because we can use it to implement an AND, OR, and NOT gate. Given an arbitrary gate, or set of gates, how many operations would it take to verify if ...
0
votes
1answer
39 views

For a logic gate to be universal, must it necessarily be able to perform duplication?

It is said that a gate that can simulate AND and NOT is universal and able to recreate any classical circuit. I was looking at some of the circuits simulated by NAND, and for some of them, we need to ...
2
votes
1answer
25 views

first order logic to normal form order of operations

∃y∀x [A(x) ∧ B(y) -> C(x,y)] ∃y∀x [¬(A(x) ∧ B(y)) v C(x,y)] ∃y∀x [¬A(x) v ¬B(y) v C(x,y)] I need to convert the above to conjunctive normal form. I'm a ...
0
votes
1answer
36 views

Lambda calculus simplification excercise

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. (λx.λy.yx)z (λw.w) I am lost with this. if anyone could lead me in ...
1
vote
1answer
40 views

Universal Quantifiers in QBFs

I've been looking into reductions to/from the TQBF language and have managed to get stuck on something that is almost certainly not true (or, if it is true I'm missing a significant computational cost ...
1
vote
1answer
23 views

For given reduction f, can show “if f(x) in 4NAE then x in 3SAT”, but not “if x is not in 3SAT then f(x) not in 4NAE”

Claim: $3SAT \le_p 4NAE $, where reduction $f$ is defined as such: given a 3CNF formula $\varphi$, add to each clause a new literal $z$ (where $z$ is same literal for each clause), and return new ...
0
votes
0answers
23 views

Two variants of Fredkin gate

Sometimes two outpus of Fredkin gate are swapped when constant bit is 0, sometimes when it is 1. What variant is right or more modern? If it was conscious decision to change behavior what was ...

1
2 3 4 5
17