Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

2
votes
0answers
160 views

Recursive definitions, How it is done?

I read that recursive definitions, refer to the definition of a function in that function body, cannot be done in $\lambda$-calculus, but recursion can be achieved by using $Y$ combinator. As I know, ...
2
votes
0answers
71 views

Unification algorithm - need clarification

I have these two terms: {P(a,x,x),P(a,b,c)} I'm supposed to find if the terms and unifiable using the unification algorithm. I'd do the following substitutions: b/x, resulting in : {P(a,b,b),P(a,b,...
0
votes
1answer
134 views

Why does (y < 10) imply everywhere (x > 0 ^ y < 10)?

My lecturer recently released solutions to an assignment. One of the questions was to determine the weakest precondition of: ...
5
votes
0answers
119 views

Characterization of alpha-equivalence in languages with bindings

Following up on this post denoting $(x \leftrightarrow y)$ the permutation of $x$ and $y$ and $P[x \leftrightarrow y]$ the term obtained from the term $P$ by permuting $x$ and $y$ (so for example if $...
7
votes
1answer
445 views

Algorithm for deciding alpha-equivalence of terms in languages with bindings

I am interested in the alpha equivalence relation in languages with variable bindings, such as: ...
2
votes
0answers
68 views

How to know whether a formula is common knowledge in Kripke structure?

Suppose that we have a formula A which is valid in all states of Kripke structure and some transition relations. Is it generally possible to derive if formula A is common knowledge between particular ...
2
votes
1answer
114 views

First Order Logic : Predicates

I have a small problem with the first order logic, in particular, predicate logic Let us take this sentence as an example: ...
3
votes
1answer
715 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
1answer
72 views

How to negate this one?

How can I negate the following sentence: For all words x from L with |x|>= n , exists decomposition x = uvw with |uv| <= n and |v| >= 1, so for all i >= 0 , is valid that u(v)^iw in L is.
1
vote
0answers
81 views

Computing critical pairs, confluence and Normal terms

Down below is a Term rewriting system where I am trying to find the critical pairs, decide if it is confluent and find the Normal terms. I think it's difficult to understand all these concepts and I ...
1
vote
0answers
205 views

Propositional logic in an SMA* algorithm

I'm trying to implement an SMA* graph search algorithm that I found in a paper here(Rong Zhou, Eric A. Hansen: Memory-Bounded A* Graph Search. FLAIRS-02 Proceedings 203-209) and I would like to ...
1
vote
2answers
284 views

Induction rules for reflexive, transitive closure

I'm trying to solve an exercise on inductive definitions, the premiss is: Let $\to$ be a relation on $A$ and $\to^*$ its reflexive, transitive closure, which is defined by following two rules: $a \...
1
vote
1answer
62 views

Secretary Problem with 2 positions - Maximizing the difference

Synopsis Imagine the secretary problem, except the goal is to hire two secretaries with the greatest possible difference between the two. The Problem I'm not particularly comfortable with this ...
2
votes
1answer
73 views

Are these examples of unification problems?

I have been studying unification, especially nominal unification (paper) gets my attention. I read the theory and examples. But I am wondering that what kind of problems occur in unifications. For ...
1
vote
1answer
427 views

Why does radix sort work?

I understand how radix sort works and how to implement it, but I don't understand why it works. Are there any underlying mathematical or logical principles that it relies on?
1
vote
1answer
40 views

Building a verifier for sentences involving addition over the natural numbers

Consider the model $(\mathbb{N},+)$; that is, the natural numbers equipped with the addition relation, PLUS($x$,$y$,$z$), where PLUS($x$,$y$,$z$) is true iff $x + y = z$. Let Th$(\mathbb{N},+)$ be the ...
1
vote
0answers
117 views

Understanding quantifiers

I'm reading a paper by David Monniaux An encoding of array verification problems into array-free Horn clauses. Second page Line 10: "Very often, desirable properties over arrays are universally ...
2
votes
0answers
95 views

Satisfying of $\square (\neg A \cup B)$

Let's consider the following formula: $\square (\neg A \cup B)$. Does the following computation satisfy it? The numbers in brackets are number of state. (0) $\neg A, \neg B$ (1) $\neg A, B$ (2) $...
2
votes
1answer
82 views

Showing $1$-reducibility of $\overline{\text{HALT}'}$ to index set

Note: overline denotes complement I am trying to show that $\overline{\text{HALT}'}\leq_1 \{i\colon\Phi_i=\Phi_e\}:= A$ for some fixed $e$ but I am misunderstanding the problem or method and can't ...
1
vote
1answer
74 views

What kind of LTL formula can be represented by DBAs

I am looking for the portion of LTL formula that can be expressed by deterministic buchi automata. Is there any classification of this such?
3
votes
1answer
180 views

Expressing a logical constraint in integer programming

Let $x$ be an integer such that $x \in [ - 10,10]$ and $b$ a binary variable. Apply integer programming to express $b = 1 \leftrightarrow x \ge3$ My work: \begin{equation} \begin{cases} \...
0
votes
0answers
31 views

Valid parenthesis Matching in MSO

What is the Monodic Second Order formula that encodes all binary strings that represent a valid parenthesis matching ? By this I mean 1s represent '(' and 0s represent ')' and at every position, ...
3
votes
1answer
64 views

Encoding first order formula (or its tree) into binary string?

How to encode a first order formula into binary string, which I could give as input to Turing machine or program to do something with it (deciding is it satisfiable, or is concrete structure model for ...
2
votes
1answer
146 views

Simplifying this Boolean Expression

I have to simplify A+C'+B'CD but I don't see how. I had to deduce the expression starting from a logic diagram in which two AND gates were used for the B'CD part. Seeing the diagram all I can think ...
1
vote
2answers
115 views

Expressing the condition as a set of linear constraints

Express the condition "$x = 0$ if and only if $y = 0$" as a set of linear constraints, where $x,y$ are integers such that $ - 5 \le x \le 8$ and $0 \le y \le 1$
3
votes
0answers
64 views

Construct skolemform of: $\forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X, S,T))$

This question is not asking for a solution, but rather as a check / validation of my thought process. Given the form: $W = \forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X,...
9
votes
2answers
179 views

What is the current status of parallel or concurrent programs in the Curry-Howard isomorphism?

In Girard's Proofs and Types we can read : From an algorithmic viewpoint, the sequent calculus has no Curry-Howard isomorphism, because of the multitude of ways of writing the same proof. This ...
4
votes
0answers
59 views

What is the role of abstract machines in the Curry-Howard isomorphism?

By abstract machines I mean things like the SECD machine, Krivine's machine or more generally machines with states/memory/registers/stack/accumulator... According to Wikipedia page of the Curry-...
7
votes
2answers
379 views

Example of inductive sets that are neither least nor greatest fixed point

Do there exist a set of inductive rules and a fixed point of these rules but is neither the least nor the greatest fixed points?
1
vote
0answers
462 views

3 bit binary multiplier?

I have the following 2-bit binary multiplier How can I modify this 2-bit binary multiplier to make it a 3-bit binary multiplier? I notice that there are 2 half-adders, and there are a bunch of ANDs ...
3
votes
0answers
43 views

How to express modalities in rule bases, knowledge bases or expert systems?

Knowledge bases and expert systems are usually production rules systems and as such they lack expressive means for expressing modalities like "agent believes in statement", "agent has duty to perform ...
3
votes
1answer
80 views

CTL* query evaluation order

I'm currently trying to evaluate a CTL* expression and am not sure how to stepwisely evaluate the queries. For example I have EFG p. This means something like 'there is a path where eventually there ...
1
vote
1answer
22 views

Constructing logical sentences that involve negative integers over the nonnegative integers

Consider the following statement: If $x$ and $y$ are integers and $z$ is a nonnegative integer and $x + z = y$, then $x$ is at most $y$. I'd like to build a sentence for this statement in the ...
4
votes
2answers
52 views

Explanation of proof of why connectedness is not conjunctively local of any order $k$

I was reading Minsky's and Papert's book on perceptrons and I was reading theorem 0.6.1 and I was having a hard time understanding it. The theorem was about proving that the property "connected" was ...
3
votes
1answer
52 views

In the Resolution equivalence ($\neg A \implies B, B \implies C \models \neg A \implies C$) must $A$ be negated?

The sheet of equivalences given to us in class provides the the equivalences \begin{array}{|c|c|c|} \hline \text{Resolution} & A \vee B, \neg B \vee C \models A \vee C & \neg A \implies B, B ...
1
vote
0answers
33 views

What does the structure ($S_t^x P$) in this Existantial Instantiation imply, Skolemization?

The sheet of equivalences given to us in class provides the two equivalences \begin{array}{|c|c|c|} \hline \text{Universal Instantiation} & \forall x ~ P(x) \implies {S_t}^x P & \exists y ~ \...
2
votes
1answer
35 views

How would one construct conjunctively local predicate of order k for checking if a shape is Convex?

I was reading Minsky's and Papert's book on perceptrons and it had the definition of conjunctively local as follow (look at the last images if its still unclear): A predicate $\psi$ is conjunctively ...
0
votes
2answers
95 views

Is 2QBF in P^NP?

2QBF is the following problem: given a CNF formula $\psi$ on $2n$ variables, determine the truth value of $$\forall x \in \{0,1\}^n . \exists y \in \{0,1\}^n . \psi(x,y).$$ Question: Is 2QBF in $P^{...
0
votes
1answer
351 views

How to simplify sum of products boolean expression?

I started with this sum of products: abc’d’ + abc’d + ab’cd’ + a’b’cd’ + a’bc’d + a’bcd + ab’c’d + a’b’c’d I have been able to simplify to this: ...
0
votes
2answers
1k views

Design a 1-bit ALU using the smallest MUX possible

Implement a one-bit ALU which takes two one-bit operands $a_0$, $b_0$, and produces a one-bit output $z_0$. The ALU has a two-bit control input $cont_0$, $cont_1$, with codes as shown below. |$...
1
vote
2answers
60 views

Can you apply the induction hypothesis to its outcome?

Assume a well-founded relation $<$ over a set $S$ and a property $P$ on $S$ such that: $P$ holds for all minimal elements of $S$. For every $b \in P$ and $a < b$ we have: if $P(a)$ then there ...
2
votes
2answers
145 views

basic turing machine

I'm trying to create a TM that changes all $a$'s to $b$'s and all $b$'s to $a$'s in a given string and then halts on the first blank space it encounters. What I have is: $$ \langle q_1,a,b,q_1\...
1
vote
0answers
179 views

StarCraft Map Dimensions [closed]

In StarCraft Brood War, a map's maximum dimension in either the X or Y direction is 256 cells. A map's dimension is required to be a multiple of 32. Each cell is 32 pixels in both directions (And ...
0
votes
1answer
44 views

How to conceptually represent attributes (characteristics) of an object in logics?

I am reading about/working on the knowledge representation using OpenCog framework http://wiki.opencog.org/w/OpenCog_Framework which essentially is special kind of probabilistic logic (s.c. PLN - ...
4
votes
0answers
71 views

In ontology development, where do axioms come from?

I am developing an ontology. I've got the classes, relationships and I guess I could come up with instances at this point too. But what I'm really focused on is the axioms. I've learnt that the ...
6
votes
1answer
195 views

Is there an algorithm to detect race conditions in logic circuits?

I'm writing a logic gate simulator. I would like to prevent user from constructing circuits prone to race condition such as flip-flops, and instead provide them as separate building blocks. Is that ...
1
vote
1answer
42 views

Connecting The Informal and Formal Definitions of Decidable With Each Other

From pg. 64 of Lambda Calculus and Combinators, the author formally and informally defines the notion of "decidability": 1 Formal Definition Definition 5.4 A pair of sets $\mathcal{A}$, $\mathcal{...
1
vote
2answers
62 views

What these simple rules of logical implications mean

Their are many rules of logics, predicate calculus, inferences and syllogisms which haunt me always. It feels better when I find some sensible name to particular rule which also gives me intuition ...
0
votes
1answer
96 views

Multiplexer output

The multiplexer is a device that selects one of several analog or digital input signals and forwards the selected input into a single line. Please consider a, for example, four data input multiplexer....
0
votes
2answers
229 views

When is a first-order formula is existential and when is it universal?

So I have a few questions about determining which formula it is: So if a binary predicate symbol $X$ denotes an edge between two variables, say $x$ and $y$, for the following formulas Why is $\...