Stack Exchange Network

Stack Exchange network consists of 175 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

3
votes
0answers
90 views

Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
1
vote
1answer
98 views

Given the phrase “Where NONE of the following are TRUE” and two statements how should a boolean logic be composed?

Let's have two statements (value > 10) (value < 25) And a list of items with the following values 10 20 30 This is what a truth table would give ...
4
votes
1answer
316 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. ...
7
votes
2answers
2k views

Lambda Calculus simplification

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem. $$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda sz.sz)$$...
2
votes
1answer
3k views

How to make a parse tree for the following propositional logic formula?

I have a formula $ \neg((q \implies \neg q) \vee p \vee (\neg q \implies (r \wedge p))) $. As it contains 3 subformulas between the $\vee$'s, how can i put it into a parse tree, as a parse tree ...
5
votes
1answer
247 views

How many possible assignments does a CNF sentence have?

I'm having some trouble understanding the following: When we look at satisfiability problems in conjunctive normal form, an underconstrained problem is one with relatively few clauses constraining ...
2
votes
1answer
332 views

definition of formula validity

I read in some sources that valid formulas are tautologies (valid under every evaluation). In the others, I read that these are formulas that have conclusions true when premises are true. Are these ...
7
votes
1answer
232 views

Redundancy elimination in the superposition calculus

When proving theorems with the superposition calculus, we deal with three kinds of rules: Generating rules: from pair of clauses A and B, generate new clause C while keeping the original pair, e.g. ...
2
votes
1answer
1k views

Negation of nested quantifiers

The problem is: $$\exists x \forall y (x \ge y)$$ With a domain of all real positive integers. The negation is: $$\forall x \exists y (x < y)$$ so, if $y = x + 1$, the negation is true. That ...
0
votes
2answers
370 views

Predicate Logic Paradox [duplicate]

Possible Duplicate: Negation of nested quantifiers The problem is: ∃x∀y(x ≥ y) With a domain of all real positive integers. The negation is: ∀x∃y(x < y) so, if y = x + 1 the negation is ...
6
votes
2answers
202 views

The meaning of modulo in “formula modulo a background theory”

I have been reading some papers where I keep reading stuff like “first-order formula modulo a background theory”. Does anyone know what modulo means in this case ? Is it something like “with respect ...
10
votes
1answer
447 views

Distinct variables for different clauses

In resolution theorem proving, it is normally assumed variables in different clauses are distinct. This is not something that happens automatically; it requires significant extra code and computation ...
5
votes
1answer
113 views

Is the validity of some instance of an equational problem decidable?

Is the following FOL-problem (equality is a logical symbol) effectively decidable? Given. A finite equation system $E$ and an equation $s = t$. Question. Is there a substitution $\sigma$, such ...
5
votes
1answer
301 views

Free variables of (λx.xy)x and bound variables of λxy.x

I was solving exercises on Lambda calculus. However, my solutions are different from the answers and I cannot see what is wrong. Find free variables of $(\lambda x.xy)x$. My workings: $FV((\lambda x....
8
votes
1answer
261 views

How much can we reduce the number of clauses by converting from $k$-SAT to $(k+m)$-SAT?

If we suppose that we start with an instance of $k$-SAT, and try converting the problem to an instance of $(k+m)$-SAT, where there are $(k+m)$ literals per clause, can we guarantee a reduction in the ...
8
votes
2answers
377 views

A tentative satisfiability algorithm

General satisfiability (with a few exceptions such as Horn Clauses) is not believed to have an algorithmic solution. However, the following algorithm appears to be a solution for general ...
9
votes
2answers
408 views

Introduction into first order logic verification

I am trying to teach myself different approaches to software verification. I have read some articles. As far as I learned, propositional logic with temporal generally uses model checking with SAT ...
14
votes
4answers
606 views

Is there a repository for the hierarchy of proofs?

I am self-learning proof assistants and decided to start on some basic proofs and work my way up. Since proofs are based on other proofs and so form a hierarchy, is there a repository of the hierarchy ...
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 ...
4
votes
1answer
648 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 ...
6
votes
6answers
428 views

Looking for books on creating and understanding theorems targeted at Computer Science

In studying logic to understand verifying programs I have found that there are books on logic targeted at Computer Science e.g. Logic in Computer Science: Modelling and Reasoning about Systems ...
5
votes
1answer
488 views

Period in postulate; what does it mean?

While I am learning a lot from others here at the Computer Science site, I must admit that I don't get as much out of some questions and answers since I typically don't understand the theorems to the ...
11
votes
1answer
453 views

Inferring refinement types

At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so: <...
22
votes
5answers
968 views

$\lambda$-calculus with reflection

I'm looking for a simple calculus that supports reasoning about reflection, namely, the introspection and manipulation of running programs. Is there an untyped $\lambda$-calculus extension that ...
3
votes
1answer
293 views

Operations on OBDD: negation through Shannon's expansion

I have a problem with the application of the Shannon expansion for to obtain the negation of a formula boolean, than will need for implement the negation operator on OBDD (Order Binary Decision ...
3
votes
1answer
1k views

Can truth tables be used in non-boolean algebra to derive functions?

There are obvious analogs (pardon the pun) between Boolean algebra and algebra. They have similar laws, operators and properties. I can't figure out why Karnaugh Maps and sum of products, which are ...
3
votes
3answers
242 views

Why is GFp -> GFq false in LTL, even though GFp and GFq are false?

Consider the Kripke structure: $$ \begin{array}{ccccccc} \to & (p, \neg q) & \to & (\neg p, \neg q) & \to & (\neg p, q) \\ & \circlearrowright & & \circlearrowright ...
3
votes
1answer
212 views

Time to construct a GNBA for LTL formula

I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula: Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
4
votes
2answers
636 views

What is the type theory judgement symbol?

In type theory judgements are often presented with the following syntax: My question is what is that symbol in the middle called? All the papers I've found seem to use an image rather than a unicode ...
2
votes
3answers
221 views

Is switching quantifiers allowed in this instance?

In Logic In Computer Science (2nd Edition - Michael Huth and Mark Ryan), exercise 2.4.12.k is the following: For each of the formulas of predicate logic below, either find a model which does not ...
14
votes
1answer
559 views

Type inference with product types

I’m working on a compiler for a concatenative language and would like to add type inference support. I understand Hindley–Milner, but I’ve been learning the type theory as I go, so I’m unsure of how ...
4
votes
1answer
777 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 ...
17
votes
3answers
2k views

How to read typing rules?

I started reading more and more language research papers. I find it very interesting and a good way to learn more about programming in general. However, there usually comes a section where I always ...
9
votes
1answer
309 views

Depth-2 circuits with OR and MOD gates are not universal?

It is well-known that every boolean function $f:\{0,1\}^n\to \{0,1\}$ can be realized using a boolean circuit of depth 2 (over the variables, their negation and constant values) containing AND gates ...
8
votes
3answers
374 views

Simple explanation as to why certain computable functions cannot be represented by a typed term?

Reading the paper An Introduction to the Lambda Calculus, I came across a paragraph I didn't really understand, on page 34 (my italics): Within each of the two paradigms there are several versions ...
17
votes
3answers
2k views

Can constraint satisfaction problems be solved with Prolog?

Is "party attendance" type of problems solvable in Prolog? For example: Burdock Muldoon and Carlotta Pinkstone both said they would come if Albus Dumbledore came. Albus Dumbledore and Daisy ...
4
votes
3answers
867 views

Hoare triple for assignment P{x/E} x:=E {P}

I am trying to understand Hoare logic presented at Wikipedia, Hoare logic at Wikipedia Apparently, if I understand correctly, a Hoare triple $$\{P\}~ C ~\{Q\}$$ means if P just before C, then Q ...
25
votes
1answer
972 views

Is there a typed SKI calculus?

Most of us know the correspondence between combinatory logic and lambda calculus. But I've never seen (maybe I haven't looked deep enough) the equivalent of "typed combinators", corresponding to the ...
7
votes
1answer
255 views

Why are lambda-abstractions the only terms that are values in the untyped lambda calculus?

I am confused about the following claim: "The only values in the untyped lambda calculus are lambda-abstractions". Why are the other terms not values? What does it mean for a lambda-abstraction to be ...
12
votes
5answers
10k views

Reason to learn propositional & predicate logic

I can understand the importance that computer scientists or any software development related engineers should have understood the study of basic logics as a basis. But is there any tasks/jobs that ...
11
votes
1answer
3k views

Example of Soundness & Completeness of Inference

Is the following example correct about whether an inference algorithm is sound and complete? Suppose we have needles a, b, c in a haystack, and have also an inference algorithm that is designed to ...
7
votes
1answer
255 views

Reduction rule for IF?

I'm working through Simon Peyton Jones' "The Implementation of Functional Programming Languages" and on page 20 I see: IF TRUE ((λp.p) 3) ↔ IF TRUE 3 (per β red) (1) ...
6
votes
1answer
3k views

Lambda Calculus beta reduction

I am trying to learn Lambda calculus from here and while trying to solve some problems, I got stuck. I was trying to solve the following problem (page 14, excercise 2.6 part (i): Simplify $M \equiv (...
14
votes
2answers
780 views

Confluence proof for a simple rewriting system

Assume we have a simple language that consists of the terms: $\mathtt{true}$ $\mathtt{false}$ if $t_1,t_2,t_3$ are terms then so is $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ ...
8
votes
1answer
278 views

Lambda Calculus Evaluation

I know this is a simple question but can someone show me how $(\lambda y. \lambda x. \lambda y.y) (\lambda x. \lambda y. y)$ reduces to $\lambda x. \lambda y. y$.
15
votes
3answers
3k views

Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
16
votes
2answers
354 views

Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Why is it that automated theorem provers, i.e. ACL2,...
19
votes
1answer
922 views

Types of Automated Theorem Provers

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Which are the relevant automated theorem provers? I ...
10
votes
3answers
646 views

Polymorphism and Inductive datatypes

I'm curious. I've been working on this datatype in OCaml: ...
42
votes
6answers
8k views

Learning Automated Theorem Proving

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Note that these topics are not easily digested ...