# Tagged Questions

Questions related to mathematical logic and its use in computer science

30 views

### MTBF calculation with 2 units connected in series

Me and a friend have a opinion difference regarding a question that got asked in a previous IT test. The short version: 2 units, n and ...
61 views

### Set Levels in MSOL

I'm trying to see how Martin Lof Type Theory can be encoded in Monadic Second Order Logic over trees or graphs. Specifically, how can set levels (cumulative hierarchy) a la Russel or a la Tarski be ...
35 views

### What are the differences between parse and decision trees?

I have created a parse tree for the formula: a∧¬(b∨c)∨¬d∧(¬b) successfully. I am now asked to create a decision tree for the same formula. What are the main differences between a parse tree and a ...
20 views

### How do i construct a code for this problem? [duplicate]

In a village there are n houses , some have electricity some dont. Those having electricity are labeled as 1 and others 0. Houses are arranged in a line from left to right (1 to n). let x1 x2 x3........
692 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 ...
119 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 ...
34 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 ...
84 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$...
14 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 ...
82 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 ...
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 ...
846 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 ...
37 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-...
963 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. ...
562 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 ...
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 ...
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 (...
20 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 ...
47 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 ...
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 ...
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 ...
57 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 ...
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 ...
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 ...
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 ...
42 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, ...
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 ...
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 (...
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 ...
104 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?
65 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 <...
19 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 ...
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, ...
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-...
48 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 ...
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 ...
85 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 ...
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 ...
70 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 ...
11 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 ...
65 views