Questions related to mathematical logic and its use in computer science

learn more… | top users | synonyms (1)

0
votes
0answers
31 views

Using SMT Solvers in formula checking

I'm currently working on a static analysis work in which I need to check whether a given formula is met or not. I hope the following example clarifies my requirement. Suppose we have a list of ...
-4
votes
0answers
26 views

Implication Graph for 2Sat

How do we convert $$(x, \neg y)$$ to implication? Like I know $$(\neg x, y) = (x \to y), (\neg x \to \neg y)$$
6
votes
2answers
943 views

How to read out a double negation in propositional logic

How would one verbally say ~~R where R = my program is correct? The tildes are negation symbols. I'm not sure if it just cancels out and comes out as 'my program is correct' or if it's something else. ...
7
votes
3answers
533 views

What is the relation between First Order Logic and First Order Theory?

I thought that any FOT is a subset of FOL, but that does not seem to be the case, because FOL is complete (every formula is either valid or invalid), while some FOT (like linear integer arithmetic) is ...
0
votes
1answer
49 views

Axioms - proof of halt

I am new to this forum and this is my first post. I am interested in solving a problem, but cannot find the way to think about it. If anyone can guide me through it, I would be obliged: Let F be some ...
0
votes
0answers
20 views

Stepping through a sequence of grouped logic gates

I'm performing a simulation of protein-protein interactions. I'm using Python to code logic gates as functions to model protein interactions. My model is basically a series of groups (...
0
votes
0answers
18 views

Draw the Logic Diagram using Half-Adders to implement a ripple-carry addition for the increment

Draw the Logic Diagram using Half-Adders to implement a ripple-carry addition for the increment.(Designing the incrementer circuit for the picture below) Having a tough time drawing out this logic ...
3
votes
1answer
44 views

Equivalent formulae with different CNF

I was not able to find or come up with two formulae which are equivalent but have different CNF. All my ideas reduce to the same formula after applying transformations. The requirements are the ...
1
vote
1answer
51 views

Boolean expression logic law confusion

I've been trying to attempt a particular question that I need to translate truth table into boolean expression but I'm completely stuck on one point now. First, I worked it out by using Sums of ...
3
votes
1answer
55 views

Why do presenttations of proof systems in logic and automated reasoning not include the algorithm that finds proofs?

Is is that a common way to present a proof system in the field of Logic and Automated Reasoning is to present a system of inference rules, without having to formally describe a particular algorithm or ...
1
vote
0answers
48 views

Modal logic axiom S4, transitive and reflexive frame, tableaux solver

I have a difficult problem to solve which as mentioned in the title is related to modal logic axiom S4. So, here is some background knowledge that can be useful: S4 axiom is a class of transitive ...
2
votes
1answer
30 views

What is a local inference system?

A inference system is a set of rules that can be used to prove something in some formal model. I understand that. But what does it mean to a inference system to be local? For instance, in the page ...
2
votes
0answers
119 views

on `On the cruelty of really teaching computing science' [closed]

Dijkstra, in his essay On the cruelty of really teaching computing science, makes the following proposal for an introductory programming course: On the one hand, we teach what looks like the ...
2
votes
1answer
30 views

About a universal (functionally complete) function producing a constant

I read in a note the following: Suppose we have a boolean function $f(x,y,z,w)$, if $f(a,a,a,a)=1$ then $f$ can't be functionally complete. Why is that? how does it imply that $f$ can't produce ...
3
votes
0answers
41 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, ...
0
votes
0answers
24 views

Constructing a 4 input (Parity Checker) using only 4-input AND Gates and 2-input NAND Gates

I am struggling to construct logic gates that 4 input A xor B xor C xor D that would normally just take 3 XOR Gates (much like a parity checker), but I need to only use 4-input NAND Gates and 2-input ...
3
votes
1answer
44 views

The language of Logical Theory as Metalanguage

I am reading the Handbook of Satisfiability, and in Chapter 1 (History of Satisfiability), I found the following statement: Moreover, necessary and possible are predicates of the metalanguage ...
4
votes
1answer
61 views

What are predicates of a sentence?

I am reading Handbook of Satisfiability in which they say: An algebraic structure, or simply structure, consists of a non-empty set of objects existing in the world $w$, called the domain and ...
4
votes
4answers
94 views

XOR two numbers

Is there an intuitive meaning of XOR of two numbers not involving binary and just decimal? Or is is always converted into binary and then XORed?
1
vote
1answer
51 views

Simplifying Boolean Expression

I am designing a 4-bit comparator with a look ahead unit using a bit slice approach. I have to break the propagation of the Logical expressions for (A<B)i and ...
0
votes
0answers
16 views

How BDI agent can select next step (action)?

I am reading now about BDI (Belief-Desire-Intention) agents. I guess that this type of agents is the most popular model of cognitive agents and agents of multi-agent systems. Of course I am reading ...
0
votes
1answer
36 views

Question on interpreting logical notation, relating to alphabets, theoretical comp sci

$\exists x \in \Sigma^* (t=sx)$ Have I interpreted the above into words correctly?: "There exists a symbol 'x', which is a member of the set which contains all possible strings of alphabet sigma, ...
0
votes
1answer
25 views

Datalog - Single Step Operator

I am currently taking a class called Logic for Computer Scientist. During the first four weeks or so now we have been studying a concept Datalog with subsections Syntax and Formal Semantics and ...
1
vote
1answer
44 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
38 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
80 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
70 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
60 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
53 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
27 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
65 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
44 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
36 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
655 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
31 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
111 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
64 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
65 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
97 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
61 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
126 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
146 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
104 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 ...
18
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
72 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 ...
2
votes
1answer
92 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 ...