Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
5
votes
1answer
234 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 ...
5
votes
1answer
199 views

Lambda calculus as the language of universal logic - connectives vs functions in lambda calculus?

I am reading http://okmij.org/ftp/gengo/applicative-symantics/AACG1.pdf and there is defined language TL (see last row in the table on page 4). It seems to me from this definition of TL, that lambda ...
5
votes
1answer
141 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 ...
5
votes
1answer
201 views

Finding a graph-theoretic representation of expressions in Boole's algebra

I just read "Boole's Algebra Isn't Boolean Algebra" by Theodore Halperin (behind a paywall here). I don't have a strong background in abstract algebra, so, frankly, the paper is a bit over my head but ...
5
votes
1answer
299 views

Abduction in ASP

Well, forgive my ignorance about the matter as I have been playing with ASP for the last couple of days. Consider this simple example p. s :- p. And the ...
5
votes
1answer
1k views

Validity of predicate logic formulas

The following predicate logic formula is invalid (i.e. not a tautology): $\Bigl[\forall x \,\exists y {\,.\,} P(x,y)\Bigr] \implies \Bigl[\exists y \, \forall x {\,.\,} P(x,y)\Bigr]$ Which of the ...
5
votes
3answers
219 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 ...
5
votes
1answer
89 views

proving program equivalence

I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
5
votes
1answer
86 views

How come correctness proofs aren't tautological?

Consider the following function on binary trees, which is supposed to tell whether a given int is a member of a binary tree t: <...
5
votes
0answers
134 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 $...
5
votes
2answers
215 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, ...
4
votes
5answers
3k 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?
4
votes
2answers
14k views

The difference between a sequence and a set

I am new to discrete mathematics and the theory of computation I am trying to learn and understand the terminology. I am having a difficult time understanding the difference between a set and a ...
4
votes
2answers
279 views

First-order logic arity defines decidability?

I've read first-order logic is in general undecidable, and that could be decidable only when working with unary operators. (I think that's propositional logic, correct me if I am wrong) The question ...
4
votes
1answer
706 views

Question on the “Tutorial implementation of dependently typed lambda calculus”

I have a slight technical struggle with this marvelous tutorial. On page 5 the tutorial talks about typing rules for Simply Typed Lambdas and presents following judgement as derivable via rules on ...
4
votes
1answer
1k views

What is the difference between strong normalization and weak normalization in the context of rewrite systems?

In the context of rewriting systems, how does strong normalization differ from weak normalization?
4
votes
1answer
2k views

Consistency and completeness imply soundness?

I understand that soundness implies consistency. Also, I understand that consistency alone does not imply soundness. But shouldn't consistency + completeness imply soundness? Scott Aaronson in his ...
4
votes
3answers
2k views

Howto formally go about proving that two LTL formulas are equivalent?

Do they need to "unwind" exactly to the same set of paths or does it suffice when one set is contained in the other ? Or is it sufficient to argue that M,s satisfies both LTL formulas for any ...
4
votes
2answers
275 views

Is there a way to convert a program into a Boolean formula?

Let's say I have a program P, in form of a binary code for x86 architecture. I want to find a Boolean formula F (in form of CNF, or something like that), such ...
4
votes
2answers
563 views

Proof of Trakhtenbrot's theorem

In the proof of Trakhtenbrot's theorem (as given in "Elements of Finite Model Theory" by Leonid Libkin), for every Turing machine $M$, author constructs a FO sentence $\Phi_M$ of vocabulary $\sigma$ ...
4
votes
1answer
2k views

Propositional formula in DNF can be decided in polynomial time?

For a given propositional formula f in DNF, one can decide in polynomial time, if the formula is satisfiable: Just walk through all subformulas (l_1 and ... and l_k) and check, wheter it has NO ...
4
votes
3answers
1k views

Soundness and completeness w.r.t. programming languages

I'm studying programming languages (more specifically type systems) and came across a concept I couldn't quite wrap my head around: soundness and completeness. I'm taking a class, and according to my ...
4
votes
1answer
106 views

A universal operator necessarily generates $\neg x$ for input $x,…,x$

I originally posted this on math.stackexchange, but then deleted it and moved it here since I think it would fit this site more. I saw a claim in a slideshow from a basic computer architecture course ...
4
votes
1answer
270 views

Semantic readings of the Lambek sequent calculus

I am reading Categorial Grammar: Logical Syntax, Semantics, and Processing by Glyn Morrill and I am stuck with the Fig. 3.9: Can someone explain this set of formulas and |.| function specifically? ...
4
votes
1answer
331 views

Abstract algebra and programming languages

Quite often, I stumble upon abstract algebra concepts like initial algebra, free algebra, and similar while reading papers on programming languages. For instance, in papers on algebraic data types, ...
4
votes
1answer
225 views

Solving SAT using tableau calculus

I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ...
4
votes
2answers
312 views

Unification — most specific unifier

In unification, given a set of equations, a standard problem is to compute a most general unifier (mgu). I am interested in a somewhat reversed problem. Imagine having a set of equations that do not ...
4
votes
2answers
225 views

TQBF as interactive game

My teacher describes true quantified boolean formula (TQBF) as an interactive game between two players $\exists$ and $\forall$, and asks us to show a winning strategy for the existential player $\...
4
votes
1answer
144 views

How logic programming (especially ASP) is related to the reasoning in (first-order) logic?

How logic programming (https://en.wikipedia.org/wiki/Logic_programming, especially answer set programming) is related to the reasoning in the (first-order) logic? Maybe logic programming can be ...
4
votes
1answer
289 views

How do you represent LISP as mathematical / logical model?

I asked this in stackoverflow, but the question probably fits here better. This question arose from the objection that LISP is regarded as a functional language with some simple principles, namely ...
4
votes
2answers
88 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 ...
4
votes
2answers
282 views

Why is the assignment rule the way it is in Hoare Logic?

Why is the assignment rule the way it is in Hoare Logic/Axiomatic Semantics? I can't wrap my head around why the assignment rule is backwards from what I expected. I understand Hoare logic is use to ...
4
votes
1answer
1k 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 ...
4
votes
1answer
84 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
2answers
630 views

What is the definition of a $\Pi_1$-sentence?

What is meant when somebody says that a problem can be expressed as a $\Pi_1$-sentence? I know that for the arithmetical hierarchy, a $\Pi^0_1$-sentence is a sentence of the form $\forall n_1\forall ...
4
votes
1answer
930 views

Resolution complexity versus a constrained SAT algorithm

EDIT: ad hoc speed-ups are excluded. We have the result that propositional resolution requires exponential time. The resolution result uses the proof of the pigeonhole principle as an example of a ...
4
votes
2answers
165 views

Predicate Logic - Natural Deduction; Assumptions about exists-elimination

I am stuck on how to progress with this proof; i cannot see my next move. The task is to show $S \to \exists x Q(x) \vdash \exists x (S \to Q(x))$ using natural deduction for predicate logic. My ...
4
votes
1answer
187 views

Does Herbrand's theorem mean any first-order logic formula can be expressed in CNF?

Herbrand's theorem shows that any formula of first-order logic can be expressed as a disjunction of quantifier-free formulas of first-order logic. Is this equivalent to saying that Herbrand's theorem ...
4
votes
2answers
88 views

Temporal logic for interface invariants

I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available ...
4
votes
2answers
262 views

Creating a logical circuit

Task: Design a 2 bit comparator. Input: 2x 2 bit (I take it as 2 2-bit values, let them be unsigned for simplicity) Output: 1 if result input1>input2 is true, 0 otherwise Develop truth table and ...
4
votes
1answer
353 views

Universality of NOT and CNOT

I'm trying to figure out why NOT and CNOT gates are not sufficient to create all bijective functions in classical circuits. I have been struggling on this for hours, and just can't make sense of it. ...
4
votes
1answer
250 views

Logical characterization of P versus NP problem (and references for least fixed point logic)

Wikipedia says the following (and more) about the logical characterization of the P versus NP problem here: Thus, the question "is P a proper subset of NP" can be reformulated as "is existential ...
4
votes
1answer
144 views

SAT Solver Front-End: Strategy to order Quantifiers

I am working on a small project. The goal is to implement a compiler from a quite simple, custom syntax of logical formulae (including variables over finite domains) to conjunctive normal form (CNF). ...
4
votes
1answer
98 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
4
votes
1answer
470 views

in refutation (resolution) can we use a clause that have been resolved

In resolution if we have a set S composed of three clause C1, C2 and C3 and we want to proof that C4 is derivable from S using refutation: suppose we've resolved C1 and C2 to C5, can we resolve C1 ...
4
votes
1answer
296 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 ...
4
votes
1answer
419 views

Is There a Programming Language That Embraces Globals?

All programming languages have globally defined symbols. While best practices invariably abjure their use as mutable entities the philosophy of what is mutable and what is not mutable is highly ...
4
votes
1answer
98 views

First Order interpretation of arbitrary structures as a graph

I am currently trying to get some intuition on the concept of First Order reductions, and have come across this exercise question by Immerman, dubbed "Everything is a Graph". Given some arbitrary ...
4
votes
1answer
78 views

Showing that a Particular Word Problem is Decidable

I need to give an algorithm to show that the word problem in the group $\langle x,y \mid \mid x^{1984} = y^{2014} = 1 \rangle$ is decidable. How do I show this? I'm not too sure where to start.
4
votes
1answer
762 views

3CF 3-conjunctive form satisfiability

I am self studying discrete math and I am going through MIT Mathematics for CS lecture notes but they do not have solutions available. I got stuck at Problem 3.14 (pages 64-65 of this document). The ...

1 2 3
4
5
17