Questions related to mathematical logic and its use in computer science

learn more… | top users | synonyms (1)

1
vote
1answer
32 views

complexity of modal logic axioms

I am writing a paper in which I want to include complexity results for different modal logics and possibly add a reference to a specific paper. At the moment I have the following: K- no restrictions ...
1
vote
1answer
33 views

If a CSP (over a finite domain) has only linear inequalities as constraints, is it solvable in linear time?

I have an optimization problem in fuzzy logic that I want to model and solve as a CSP. If I could use only linear inequalities in my encoding, is the resulting CSP solvable in linear time? Problem ...
-1
votes
2answers
65 views

Which formula corresponds to this K-Map?

I have a K-Map and I need to figure out which expression isn't equivalent to the provided K-Map. $f(w,x,y,z) = \sum(3,7,9,11,13,15) + \Phi(4,5,6)$ We know that both options (a) and (b) are ...
1
vote
1answer
61 views

Logic formula for exactly n unique objects (no more, no less)

I have a question in Logic: If I am asked to construct a formula, using the '=' predicate, that shows that there are exactly n objects, I need to show that there are no n+1 objects, right? For ...
0
votes
0answers
54 views

What does an = sign with an x beneath it mean?

I am studying for a test in Logic right now, and saw the symbol $\underset{x}{=}$, which is used like this: $I \underset{x}{=} I'$. I've seen it in the solutions of questions like this one: Prove ...
1
vote
0answers
10 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
1
vote
1answer
29 views

Result of ANDing & ORing functions expressed as CDNF & CCNF

I came across following fact: If we AND two functions expressed as CDNF (Canonical Disjunctive Normal Form), then the result contains sum of commont minterms. For example consider two functions ...
2
votes
1answer
19 views

Why is c) a combinational circuit, but d) not?

I am doing practice after just learning what combinational circuits are, yet I am unsure of why (c) is combinational, but (d) is not. Can someone please explain to me why this is? The Solution ...
0
votes
1answer
54 views

Relations between statements involving universal quantifier, conditional and biconditional

If we consider two predicates: $b(x)$: x is a boy $c(x)$: x is clever Then, there are four statements involving $∀, b(x), c(x), →$ and $↔$ . These are below along with my interpretation of their ...
2
votes
1answer
33 views

Ripple Carry Adder

I'm new to computer science and came across an issue while learning about ripple carry adders. I'm trying to add binary 1+1+1 below (excuse the poor photoshopping). I know the answer should be ...
-2
votes
1answer
28 views

Help understaning LTL formulae [closed]

I am studying Software Engineering and I have different LTL formulas for which I have to determine if they are valid, unsatisfiable or neither. Here are the formulas : (<>[]p ∧ <>[]q) → ...
1
vote
1answer
69 views

Two's complement Using ONLY Logic Gates

How can a 4-bit two's complement operation be implemented using only boolean logic gates (AND, OR, NOR, NOT, NAND, XOR, and XNOR)? (This question was redirected to CS from Stack Overflow)
1
vote
0answers
28 views

Algorithms for logical synthesis of multiple output bits?

Karnaugh maps and the Quine–McCluskey algorithm can be good choices for coming up with fairly minimal logical expressions that match the requirements of a truth table. What if I have a situation ...
1
vote
1answer
33 views

Algorithms for logical synthesis

Let's say that I want to map some string of binary digits to a single binary digit of output, like the below: $ \begin{array}{l|l} \text{Input}&\text{Output}\\ \hline 0001&0\\ 0011&1\\ ...
-1
votes
2answers
40 views

How to simplify boolean expression? [closed]

I am having trouble simplifying logical expressions to a much simpler form, can someone provide me some insight on how to approach the problem? Let's assume i have the following expression: $ABCD + ...
1
vote
2answers
54 views

Substituting two different identifiers with the same identifier in Coq - why does this work?

I'm playing around with Coq and Software Foundations and is somehow very confused by something I took for granted since forever. To prove ...
0
votes
1answer
47 views

How can you check if a 2SAT problem has a bad loop

im trying to figure out why this is true The clauses {a,b}, {b,~c}, {c,~a} constitute a 2SAT problem with an implication graph without bad loops. Can someone show me how to illustrate this and ...
-1
votes
2answers
78 views

Using natural deduction, show that: ∀x.(P (x) → Q(x)), ∃x.P (x) ⊢N ∃x.Q(x)

How I would show: ∀x.(P (x) → Q(x)), ∃x.P (x) ⊢N ∃x.Q(x) using Natural Deduction? Would I not need to know what P(x) and Q(x) are to prove soundness and completeness?
0
votes
0answers
56 views

How to express r-bounded waiting for $r=0,1,2$ in LTL and Promela?

How to express $r$-bounded waiting for $r=0,1,2$ in LTL? I'm having trouble expressing the above in LTL and translating it to Promela. I've already expressed starvation-free and mutual ...
-1
votes
1answer
27 views

Which “ID” extraction is correct?

This question related to attack on the LMAP++ the result of extracting ID from the messages. In Passive Attack on RFID LMAP++ Authentication Protocolm, page 188 ...
7
votes
1answer
112 views

Understanding of Turing's Answer to the Entscheidungsproblem

I apologize if this question has been asked before, but I was not able to find a duplicate. I have just finished reading The Annotated Turing and I am a bit confused. From what I understand, the ...
4
votes
1answer
144 views

What does Godels Incompleteness theorem “true but unprovable” mean?

I have asked this on the "computer science chat" ( vzn tried to explain me ) . I even watched a couple a videos to understand the theorem but still cannot convince myself. The following is the way the ...
5
votes
1answer
97 views

Is there a decidable problem which has a proof that it cannot be proved to have a particular deciding Turing machine?

I came across the question Is there an algorithm that provably exists although we don't know what it is? I was able to follow the example "Given an integer $n\ge0$ is there a run of $n$ or more ...
15
votes
2answers
4k views

Is it possible to write an AND gate using XOR gates?

How could I express an AND gate using only XOR gates ?
5
votes
1answer
60 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
1
vote
1answer
45 views

How to XOR two binary numbers having different lengths?

If we have: x = 1101 and y = 101 How to XORing these numbers?
1
vote
1answer
20 views

What does $\alpha_r\supset\beta_r$ mean in the tolerance definition of System Z?

I'm reading up on System Z introduced by Judea Pearl (in System Z: a natural ordering of defaults with tractable applications to nonmonotonic reasoning). A central definition is that of tolerance of a ...
3
votes
1answer
276 views

Can OR be “undone”?

Suppose that $Z = X \vee Y$, where $X$, $Y$ and $Z$ are 96-bit binary numbers. If I'm given the values of $Z$ and $Y$, is it possible to work out what $X$ is? I know this is possible ...
1
vote
1answer
39 views

Non-deterministic algorithms and Tautologies

I am studying the lecture The Complexity of Propositional Proofs. ​Here there is a definition together with a discussion (page 3). I don't understand that discussion. Let $F$ denote the set of ...
1
vote
1answer
54 views

Size of Propositional Formula

I am study this lecture The Complexity of Propositional Proofs. Here there is a term size of propositional formula (page 2), Every tautology $\tau$ on $n$ variables has an $F$-proof in which ...
2
votes
2answers
66 views

What is the natural language of computers mathematics or logic? [closed]

I was reading about the history of computers where i came by machine code A Machine code or machine language is a set of instructions executed directly by a computer's central processing unit ...
4
votes
0answers
42 views

Direct conversion from regular expression to MSO

A language $L \subseteq \Sigma^*$ can be described by a regular expression iff it can be defined by a formula in monadic second order with words as structure $(\{0, \dots, n-1\}, <, (P_a)_{a \in ...
1
vote
1answer
81 views

How is the complexity/size of a problem (for instance SAT) determined?

We say an algorithm runs in polynomial time if it is of the form $O(n^k)$ where $n$ is the size of the input, right? So how do we judge how many inputs there are in: $(x_1 \vee x_2 \vee ...
0
votes
0answers
51 views

Prove the validity of a sequent (propositional logic)

At the moment I'm reading about logic in Computer Science. I have come across this excercise: and wondered if somebody could help me / explain to me how to solve this exercise. I'm using a book ...
0
votes
1answer
175 views

Implementing a Boolean function with NOR gates

Implement f(a, b, c, d) = Σ m(3, 4, 5, 6, 7, 11, 15) as a 2-level gate circuit (a) Using OR gates and NOR gates. (b) Using NOR gates only. I have found that F=ab+d using Karnaugh map. I have ...
1
vote
1answer
46 views

What can be concluded from a full application of resolution?

I know that resolution is refutation complete, but what can we conclude if a resolution procedure leads to a situation with no more chance to operate the resolution? Given a propositional formula ...
1
vote
2answers
62 views

How can I infer inputs to a function, given an output?

Is there a way to generate a set of inputs, for a given output of a function? This may be a common thing in lisp/haskell world, but I'm not aware of it. Is this what mini-kanren does? I understand ...
0
votes
1answer
49 views

Minimum number of steps to sort 3x3 matrix in a given way

So I started practicing some algorithms and programming before university starts and I ran into this problem: Given a 3x3 matrix containing the numbers from 0 to 8, find the minimum number of steps ...
9
votes
1answer
134 views

Term rewriting; Compute critical pairs

I have tried to solve the following exercise but I got stuck while trying to find all the critical pairs. I have the following questions: How do I know which critical pair produced a new rule? How ...
2
votes
1answer
38 views

Why precondition strengtening is sound in Hoare logic

I have problem with understanding why precondition strengthening is sound rule in Hoare logic. The rule is: $$ {P \implies Q, \{Q\} C \{X\} } \over {\{P\} C \{X\}} $$ I really do not understand why ...
-1
votes
1answer
73 views

Why decision problem definition ignores Gödel incompleteness theorem?

The following question assume that the decision problem definition (syntactic) has been written (and could be changed if it isn't able) to catch a concept (meaning, semantic) which has both nice ...
0
votes
1answer
85 views

Rewriting gates such as XOR into three basic gates? [closed]

How would I rewrite an XOR gate into the three basic logic gates (AND, OR, NOT). To be more specific, I have to write it in such a way with 2 NOT gates, 2 OR gates, and 1 AND gate. I also have to do ...
0
votes
2answers
181 views

Operator precedence in propositional logic

there is some kind of priorities for the elements in propositional logic ? for example : p ∧¬q → r , given this ,we there may be two options (p ∧¬q) → r OR p ∧ (¬q → r) , which one is the correct ...
2
votes
4answers
7k views

How to construct XOR gate using only 4 NAND gate?

XOR gate, now I need to construct this gate using only 4 NAND gate ...
3
votes
1answer
31 views

Extended version of the theory of reals and its decidability

It is well-known due to Tarski that the theory of reals $(\mathbb{R},+,\cdot,<,=)$ is decidable. I was asking my self whether one would lose the decidability by adding all real constants. More ...
8
votes
2answers
94 views

Assignment to make formula unsatisfiable

Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
1
vote
1answer
127 views

Intuition behind F-algebra

I looked at here for getting an intuition about F-algebra, but I am still left with some questions. Suppose I have a group signature as $\Sigma= (* : X \times X \rightarrow X, \thicksim: X ...
2
votes
0answers
28 views

Parameterized complexity of Weighted Satisfiability with few variable occurrences

Given an integer $k$ and a Boolean CNF Formula $\phi$, Weighted Satisfiability asks whether $\phi$ is satisfiable by a model of weight $k$, i.e., a model that sets at most $k$ variables to true. This ...
1
vote
1answer
80 views

m-functions in Turing's paper “On Computable Numbers and applications…”

I was reading Alan Turing's paper "On Computable Numbers with an Application to the Entscheidungsproblem". I was reading well until I encountered "4. Abbreviated Tables", page 235-236, where Turing ...
1
vote
1answer
82 views

Formalizing self-propagating behaviour

Since reading Ken Thompson's Reflections on Trusting Trust I am trying to formalize the idea of a program which mutates its own behaviour; specifically, a program that would be self-reproducing except ...