# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

664 questions
20 views

### Unclear logic notation for PFX program rules

I'm very new to this so please bear with me. I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the ...
33 views

### Operation with second-order logic formulas

I have one or more second-order logic formulas that correct for some finity model. What operation can I perform on them, so that resault is also correct for some finity model? Just conjunction is ...
39 views

### Can agent be autonomous without having consciousness?

My intuition is that 1) self-awareness (modeled through epistemic modal logics); 2) goal reasoning (e.g. https://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12292) and 3) consciousness (e.g. ...
36 views

### How to apply Hoare Logic to this function

I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to ...
51 views

### How to apply Operational Semantics to this function

Say I have a function like this: ...
58 views

### Subtlety of a bar in introduction rule

I am going through the following lecture notes by Frank Pfenning : http://www.cs.cmu.edu/~fp/courses/15317-f17/lectures/02-natded.pdf In page no 5 I cam across the introduction rule . The rule ...
33 views

### Provide a derivation from backwards on?

Suppose you have to provide a derivation by natural deduction, e.g. $((A \rightarrow B) \rightarrow A) \rightarrow A$ Is it a good advice to start from backwards on in general? I mean doing the ...
33 views

### How to express a structure of a 5-colorable graph in logic

A graph can be expressed as an structure $G = <A,R>$ satisfying the axioms $\forall xy R(x,y) \rightarrow R(y,x)$ and $\forall x \lnot R(x,x)$. How to extend the structure and/or axioms to ...
20 views

41 views

47 views

### Resolution Algorithm - No new clauses

The standard resolution algorithm returns false if no new clauses are added. I know that if $KB \land \neg a \implies []$, it returns true by proof by contradiction, but how can I understand the ...
38 views

### Expressing definite clauses (Horn rules, logic programming) in lambda terms?

There is paper which expresses lambda terms in the terms of logic programming http://www.cse.unt.edu/~tarau/teaching/PL/docs/dbx.pdf Is there conversion in the other direction - expressing definite ...
57 views

### Optimal 4-input sorting network

In his paper The Bose-Nelson Sorting Problem (1973, Chapter 15 of A Survey of Combinatorial theory on page 163 available on Google books), Knuth says that the optimal bound of 5 comparators for a 4-...
675 views

### Why is this expression (A and ¬A |= C) entailed?

Hopefully I am posting this in the right place, I am currently in a course of knowledge representation, and I came across an exercise about entailment: $$A\land\neg A\vDash C\,.$$ I would argue that ...
70 views

### Can the higher-order oracle Turing machines simulate the lower-order machines so that the current oracle does not contradict the simulated oracle?

Here is a quote from the Source 1: For example, if $M$ is a machine with an oracle for the halting problem, then obviously there isn't in general an equivalent machine that can simulate the ...
127 views

117 views

### Is this possible to solve satisfiability by using Quine McCluskey algorithm to simplify the whole given boolean formula by simplifying subformulas?

In this question Farewell Stack Exchange suggested to use karnaugh maps to solve the satisfiability problem by simplifying the entire/whole boolean formula by simplifying subformulas until you have ...
1k views

### Which of the following expressions is TRUE if and only if NOT all three variables a, b, and c have the same value?

I am trying to solve this problem and I am stuck. I think it is B, but I think I'm wrong. Thanks. Which of the following expressions is TRUE if and only if NOT all three variables a, b, and c have ...
1k views

### Finding weakest precondition

I have the following program x := y + 1; if (y > 0) then x := x + y else x := y + 100; x := x + y; I want to compute the weakest precondition for getting <...
108 views

### LTL Until Tautology

Today I had to prove some tautologies as an exercise, one of them was: (Ga)->(Fb) equivalent aU(b v ¬a) It is clear that I have to prove the implication in both ways. After putting into negation ...