Questions related to mathematical logic and its use in computer science

learn more… | top users | synonyms (1)

4
votes
2answers
634 views

Predicate Logic Notation: What does a “dot” mean?

What does a dot (.) mean in predicates? $\forall a \in A. \exists d \in D. H(a,d)$ Especially, how is the above different to $ \exists d \in D. \forall a \in A. H(a,d)$ I've never seen this used ...
1
vote
1answer
109 views

How to choose between UC and PL when using the DPLL algorithm?

We know DPLL algorithm is backtracking + unit propagation + pure literal rule. I have an example. There is one example to solve following Satisfiability problem with DPLL. if assign of "0" to ...
4
votes
0answers
32 views

The difference between dynamic logic and temporal logic

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

Universal quantification in description logic

I'm struggling to understand the universal quantification operator in description logic. Here is an example of the problem: given the DL concept $\forall R.A $ (where $A$ is an atomic concept and $R$...
0
votes
0answers
13 views

How to introduce modal reasoning in knowledge bases (Cyc, ConceptNet, WordNet)?

Is it possible and how to introduce modal reasoning in knowledge bases (Cyc, ConceptNet or WordNet). Especially I am interested in CyC (OpenCyc) - is it possible to introduce modal operators in this ...
4
votes
2answers
76 views

Is there a relationship between “sound and complete” in logic and “type safety” in PLs?

I've been wondering if there's a connection between "good logics" and "good programming languages". It seems that logics are shown to be "locally sound and complete" whereas programming languages are ...
0
votes
0answers
16 views

Using specified logic gates, how to get an exact output

So, I'm working on the decoding logic of a cpu, and I'd like to know if there is a methodology to know how many logic gates do I need and how to use them... Like for example, I have an architecture ...
11
votes
1answer
844 views

Testing whether an arbitrary proof is circular?

I was thinking about proofs and ran into an interesting observation. So proofs are equivalent to programs via the Curry-Howard Isomorphism, and circular proofs correspond to infinite recursion. But we ...
0
votes
0answers
34 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 three-...
6
votes
2answers
961 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
552 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
50 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
46 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
61 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
51 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
32 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
121 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
25 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
102 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
61 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
17 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
27 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 Fixed-...
1
vote
1answer
47 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
84 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
75 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
68 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
57 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
29 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
69 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
38 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
820 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
33 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
135 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 + A\...
1
vote
2answers
65 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
66 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
100 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 exclusion. ...
-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 ...