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

2
votes
1answer
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 ...
1
vote
1answer
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 ...
1
vote
1answer
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. ...
1
vote
0answers
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 ...
0
votes
1answer
51 views
2
votes
2answers
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 ...
0
votes
1answer
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 ...
1
vote
1answer
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 ...
0
votes
0answers
20 views

Why are there so many different computer programming languages? [duplicate]

This is for a school project, please help. I have looked this up, but haven't gotten a good answer.
-2
votes
1answer
41 views

What is Control ROM and Decision ROM?

I have done some research but I cannot answer this question. Please Help.
1
vote
1answer
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 ...
3
votes
0answers
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 ...
1
vote
1answer
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-...
4
votes
1answer
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 ...
1
vote
1answer
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 ...
2
votes
1answer
127 views

Trying to understand interpretation and denotation in FOL

I am going through the book "Knowledge Representation and Reasoning" by Brachman and Levesque. So an interpretation $ F $ is defined as a pair $ \langle D,I \rangle $ mapping from a set of objects $ ...
1
vote
2answers
66 views

The set of valid sentences in FO is not decidable as a consequence of rec. inseparability

Two given languages $L_1$ and $L_2$ are called recursively separable iff there exists a recursive languge $R$ such that $L_1 \subseteq R$ and $L_2 \cap R = \emptyset$. Now consider first order logic, ...
2
votes
0answers
95 views

Is there an analysis of the creation of axioms for a mathematical structure as a computational problem?

Historically, what has happened is the following: There is a "mechanical" structure, most importantly, arithmetic, which operates according to a set of well-defined rules that a stupid computer can ...
0
votes
1answer
64 views

LTL to automaton translation that can only read disjunctions of labels per transition

Is there any automaton (or automaton translation) as expressive as LTL that can only read disjunctions of atomic propositions per each transition? Standard LTL-to-automaton algorithms allow the ...
0
votes
0answers
55 views

What are transitive roles in description logic?

I've begun to study Description Logic recently and there are a huge number of new terms to me. One of these terms is transitive role. I found this term in slide 7 and my question is: what is ...
0
votes
1answer
55 views

box bottom is valid

This question was posted to me: What property of our relation $R$ between worlds must be true if we know that the following formula is valid? $\square \bot$ I am completely stumped and have no idea ...
2
votes
1answer
70 views

Complexity of Solving a System of Polynomial Equations

It can be easily seen that solving systems of polynomial (i.e. not necessarily linear) equations is NP-Hard via reduction from SAT. Furthermore, because the existential theory of the reals is ...
35
votes
3answers
5k views

What exactly is a logic?

An apology might be in due for asking another question about prerequisites, but I was confused about the starting points. I have come across various terms such as "Modal Logic", "Temporal logic", "...
10
votes
0answers
254 views

Is Agda sound as a proof system?

I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's ...
4
votes
1answer
101 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). ...
1
vote
0answers
46 views

What is the definition of the property of Canonicity for a logic?

I'm trying to understand "A Systematic Approach to Canonicity in the Classical Sequent Calculus" by Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. The article discusses a property called "canonicity" ...
0
votes
1answer
58 views

Inference rules for deriving invariants in Hoare logic

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

Classical set theory and the existence of at least one set

As a student of mathematics I used to accept the argument that the existence of the empty set followed from the axiom schema of comprehension, so long as we could prove the existence of at least one ...
4
votes
1answer
86 views

Developing invariants for comparing two strings

The following algorithm is supposed to compare two strings $S_1$ and $S_2$ ("/\" for empty string): ...
3
votes
2answers
396 views

Propositional Logic Time complexity

If i have a propositional logic formula, every time i add a variable the number of interpretation grow up by 2. So if i have a propositional formula with 3 variables i have 8 interpretations. So, is ...
1
vote
1answer
30 views

Semidecidability and NP-Hard

Im studying the semidecidability of First Order logic. According to wiki A logical system is semidecidable if there is an effective method for generating theorems (and only theorems) such that ...
0
votes
1answer
66 views

SAT solver optimizations of DPLL for unsatisfiable formulas [duplicate]

I am implementing a SAT solver based on DPLL algorithm, and it works fine on small formulas and larger satisfiable problems. My case split is based on a tree like structure, where every branch is ...
5
votes
2answers
966 views

Equisatisfiability in the reduction from 4-SAT to 3-SAT

So If I understood correctly, the conversion from 4-SAT statement to 3-SAT statement follows the following approach: (a or b or c or d) -> (a or b or z) and (-z or c or d) Where the z is a new ...
0
votes
0answers
70 views

Is it possible for a [futuristic] computer to contain the information of the whole universe?

(This is a question of information theory, data compression and entropy, so I believe it fits CS forum) Does the fact that the computer itself is a part of the universe make it logically impossible ...
18
votes
4answers
5k views

Can proof by contradiction work without the law of excluded middle?

I was recently thinking about the validity of proof by contradiction. I’ve read for the past few days things on intuitionistic logic and Godel’s theorems to see if they would provide me answers to my ...
12
votes
5answers
2k views

Why does soundness imply consistency?

I was reading the question Consistency and completeness imply soundness? and the first statement in it says: I understand that soundness implies consistency. Which I was quite puzzled about ...
0
votes
0answers
34 views

Description logic representation

If Manufacturer manufactures electronic equipment, then manufacturer generates e-waste. I have generated the triple. However how to represent the if-then statement in DL? ...
5
votes
1answer
247 views

Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence

I have to ask for forgiveness in advance if the whole question doesn't make a lot of sense, but unfortunately, I have no better intuition as of right now and this seems like the best starting point I ...
0
votes
1answer
114 views

Can the foundation of computer science be implemented to include new rules of inference so that computer can do causal reasoning?

The idea I'm thinking of is about a top-down approach for AI. I would like to know if there can be a model for computers so that they can perform causal reasoning. It seems that causal relation can be ...
1
vote
2answers
505 views

how to solve Hoare logic problems

I'm having trouble proving Hoare logic questions as I'm not sure of the process that is taken to prove them. I understand that they're rules such as assignment axiom, pre-condition strengthening, post-...
2
votes
2answers
167 views

A 4-bit combinatorial circuit that outputs 1 when integer greater than 7 and is odd number

I need to draw a combinatorial circuit that when an integer is greater than 7 and is an odd number, the output will be 1. There are 4 inputs representing 4 bits and 1 output wire. The output wire is ...
0
votes
1answer
949 views

Proof of Demorgan's law [duplicate]

how can i prove Demorgan's law (X+Y)'=X'. Y'?I already tried studying book but doesn't understand the first step so plz answer in detail.(beginner here)
0
votes
1answer
68 views

Does exist NP language that is Cook Levin deterministic reducible to xor satisfiability in polynomial time?

We say that the language $L$ is Cook Levin deterministic reducible to xor satisfiability in polynomial time if and only if for each word $w\in\Sigma^*:w\in L\iff f(w)\in XORSAT$ where $\Sigma=\{0,1\}$ ...
2
votes
1answer
57 views

Why is $AF \phi \lor \varphi$ not equivalent to $AF \phi \lor AF \varphi$?

Can someone explain to me (perhaps with an example) why $AF (\phi \lor \varphi)$ is not equivalent to $AF \phi \lor AF \varphi$. This seems counter-intuitive, because in any path where $\phi$ (or $\...
0
votes
1answer
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 ...
0
votes
2answers
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 ...
0
votes
1answer
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 <...
1
vote
1answer
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 ...
2
votes
1answer
46 views

LTL Formula Until with same atoms (aUa)

I am trying to solve some past papers in preparations for my next exam and I've stumbled across the following exercise: While I managed to solve most parts of the exercise, I am still unsure about ...
5
votes
1answer
158 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 ...