Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
0
votes
0answers
34 views

Using Hoare logic to show an invariant holds or using induction?

I want to know if given a while loop: x = 0 while(x < 5){ x = x + 1 } I want to show that x (at the a ith iteration of the loop), the value of i is ...
8
votes
1answer
500 views

Representation of the concatenation at the type level

I would like to learn more about concatenative programming through the creation of a small simple language, based on the stack and following the concatenative paradigm. Unfortunately, I haven't found ...
1
vote
0answers
63 views

Datalog Program Equivalence with Fixed Universe Size

It is well known that to compute equivalence of two Datalog programs (or equivalently of two first order formulas with the least fixed point operator) wrt all possible inputs and universes, is ...
0
votes
1answer
82 views

Confusion about assignment axiom in Hoare logic

I wanted to know if we are given the f.f.g. Hoare triple: {x = 43}x := x + 1{x = 44} How do we show that this is a valid Hoare triple? My attempt was: Using the assignment axiom: {x + 1 = 43} x := ...
0
votes
0answers
51 views

What are necessity and sufficiency?

I was reading deadlock topic from Operating Systems book by Stallings. It states four pre requisites for deadlock: Mutual exclusion No preemption Hold and wait Circular wait It then have following ...
2
votes
0answers
134 views

Second Order QBF

Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first ...
1
vote
1answer
54 views

Substructural Prolog?

Substructural logic is logic without some or all of the structural rules. Is substructural Prolog, substructural logic programming possible? My question is connected with article https://link.springer....
2
votes
1answer
231 views

Create NOT gate from other gates

If we are given only one NOT gate and any number of OR and AND gates, then, can we simulate more NOT gates?
1
vote
2answers
107 views

Are $\mathsf{\#P}$ problems harder than $\mathsf{NP}$ problems

I have a method to solve the $\mathsf{\#P}$ version of 3SAT in a way that seemingly reduces it to an $\mathsf{NP}$ problem. - I don't have a formal understanding of these terms so I will just show an ...
1
vote
3answers
160 views

Can undecidability theorems be detected by a machine? [closed]

this question was originally written in mathoverflow, but a comment recommended me to rewrite it as a CS question. This is not a mathematically formalized question. I'm sorry for that but think it's ...
2
votes
1answer
73 views

3-CNF to “independent form”

Is it possible to convert all logical formulae into a form such that each variable ends up in exactly 1 "factor" of the and operation? ($\wedge$). Any combination of operations is allowed, though the ...
2
votes
1answer
63 views

Conjunctive normal form to simple elementary algebra

I'm curious to know the computational complexity class of each step in this method of converting a CNF formula into simple elementary algebra. An example: $$\phi=\left(x_1 \vee x_2 \right) \wedge \...
3
votes
1answer
64 views

Polynomial size Boolean circuit for counting number of bits

Given a natural number $n \geq 1$, I am looking for a Boolean circuit over $2n$ variables, $\varphi(x_1, y_1, \dots, x_n, y_n)$, such that the output is true if and only if the assignment that makes ...
2
votes
1answer
182 views

The law of excluded middle and decidability

I will divide my question in two parts. The first part I am sure that there is a objective answer, but I am not sure about the second part. First part: Is it all (decisions) problems trivial to prove ...
1
vote
1answer
82 views

Algorithm for automatic construction of natural deduction proofs

I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic. If there is no algoritm, can you ...
1
vote
1answer
80 views

Algorithm for deducing values

I have a group of logical conditions and need to deduce values that would NOT satisfy them. For example: City != New York && Location = Museum ...
1
vote
1answer
66 views

Did Wheeler really believe that physics was undecidable?

John Archibald Wheeler was a famous physicist It has been stated that he thought that there was a strong connection between undecidability and quantum physics This idea was given an early ...
2
votes
0answers
35 views

Substituting a term for a variable in a context

At this link you can read Nicola Gambino's slides on one way to approach the formal syntax of Martin-Löf dependent type theory. (They are concise and very readable.) On slide 10, he gives a standard ...
1
vote
1answer
71 views

Examples for Partial Combinatory Algebras

I am currently working on my Bachelor thesis about Turing Categories (see Introduction to Turing Categories [1]). In this context I got some questions regarding Partial Combinatory Algebras (PCAs), ...
0
votes
2answers
88 views

Prove propositional formula is a tautology [closed]

I need to show this formula is a theorem of propositional calculus. I tried assuming antecedent and proving consequent but didn't work for this proof. Do I need to show it is equivalent to true? How ...
4
votes
0answers
44 views

Is there a correspondence of steps between DPLL and sequent-calculus?

Is there a correspondence between the steps in using DPLL to find out that a formula in propositional logic is unsatisfiable and using sequent calculus to prove that its negation is valid? And given ...
2
votes
1answer
34 views

Translation of diagnosis problem to SAT

I have the following diagnosis problem: h(A): z1 = not(in1) h(D): z2 = not(in2) h(B): z3 = z1 or z2 h(C): out1 = not(z3) h(E): out2 = not(z3) This is an image of the system: I have an observation ...
3
votes
1answer
54 views

Two questions on MSO

First question : Is the following formula a valid MSO formula? $\theta(S, r) = \exists (e_1, t_1), ... ,(e_h, t_h) \bigwedge\limits_{(e_i, e_j) \in \rho(S,r)} \mathcal{R}((e_i, t_i), (e_j, t_j)...
1
vote
1answer
58 views

MSO (Monadic second-order logic) Logic On Words

Let L be a language over $\Sigma = \{a,b,c\}$ that contains all words, where the length $|w|_b$ (number of all b's) has remainder 1 if divided by 3. MSO logic over words are definded as follow: I ...
2
votes
2answers
82 views

What is the connection between the logic and the logic programming?

As I understand, then logic (i.e. particular theory of logic with some theory's axioms and some possible assignments of the variables) describes some specific world (in the non-modal case) or some set ...
1
vote
1answer
71 views

How to draw an LTS based on the parallel process “|” in CCS Milner's logic?

I'm trying to provide a Hennessy-Milner logic formula for CCS expressions that are not (strongly) bisimilar. An example with a sketch: For each of the following CCS expressions, decide whether ...
1
vote
0answers
67 views

Law as a computer science problem?

For a long time, computer scientists and logicians have noticed that law (statutes, contracts, adjudication, etc), has some similarity with formal logic and programming languages, and have approached ...
1
vote
0answers
55 views

What is this weird gate?

This came from a picture of something that I'm supposed to make, and I can't find it in the program I'm supposed to use (LogicWorks). It looks like it 'not's only one of its inputs, but that doesn't ...
0
votes
2answers
456 views

The barbers paradox first order logic formalization

I tried to look on the site and while I found some similar questions, I did not find the first order logic formalization of the following sentence (the basic barber's paradox), so I wanted to ask if I ...
1
vote
1answer
70 views

Modeling equality in an ILP

Lets say we have integer variables $a \in\mathbb{Z}^n$ and $M \in\{0,1\}^{n\times L}$. I am promised $a_i \leq L$, for some fixed constant $L$. I want to model the constraint $$M_{i,j} \iff (a_i=j)$...
0
votes
1answer
37 views

Aggregate text data of some particular column

I have a dataset as follows ...
3
votes
1answer
43 views

Efficient method for generating the smoothing function

The smoothing function of a boolean function with respect to one of its variables is the disjunction of its cofactors. For example given a Boolean function F(a,b,c) the cofactors with respect to a are ...
2
votes
1answer
53 views

Logic of multiple variables in ILP

Is there a better way to represent an AND of $n$ variables together other than creating $O(n)$ new variables and constraints?
3
votes
1answer
58 views

Basic second-order logic example contains a mistake?

I'm reading the following course on second-order logic, by Péter Mekis : http://phil.elte.hu/mekis/sol.pdf . The course seems excellent, but I'm stuck on one of his first examples for showing the ...
6
votes
1answer
132 views

How do we know $\neg \neg LEM$ isn't provable in MLTT?

I've been trying (fruitlessly) to prove something which I now know is not provable. Take the following definitions: $$LEM \equiv \prod_{A : Type} \neg A \vee A$$ $$DNE \equiv \prod_{A : Type} \neg \...
-1
votes
1answer
55 views

What is the minimum type of logical system that recognizes if a formalized sentence is a well-formed formula thus reducible to the boolean value?

The formula, in the old way of using it, can contain symbols in order and a mixture that does not meet the criteria of correctness (i.e. arbitrary symbols do not form a well-formed formula (WFF) and ...
1
vote
1answer
28 views

List of all possible reasoning tasks - satisfiability and theorem proving only?

What is the exhaustive list of reasoning tasks? As far as I can understand, then any logical reasoning reduces to 2 tasks only: 1) satisfiability problem (finding the assignment of the variables) and ...
0
votes
2answers
501 views

how do we demonstrate using Boolean algebra that these NAND and NOR gate combinations are XOR gates

How do we demonstrate using Boolean algebra that these NAND and NOR gate combinations are XOR gates?
1
vote
1answer
56 views

Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?

Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$? Attempt: In the first property each state must eventually see $\psi_1$ and $\psi_2$, in the second property as ...
0
votes
1answer
72 views

Boolean expression for sum bit of full adder

The Boolean expression I find on the internet for the sum bit of a full adder is A xor B xor Cin. Does't this expression exclude the A=1,B=1,Cin=1 situation? When that happens, the sum bit is also 1, ...
0
votes
0answers
30 views

Algorithm to find possible variables in multiple connected equations

I am new here. I am trying to come up with an algorithm that can give me the unknown values in the following equation. ...
0
votes
1answer
124 views

Hoare triple: Loop invariant and correctness

The following Hoare triple in which variable a is an array of integers, and len, max, i, n, j and m are integer-valued variables. Provide a loop invariant (using predicate logic) suitable for proving ...
2
votes
0answers
95 views

Hoare triple: Loop invariant and partial correctness

Below there is Hoare triple in which variable $a$ is an array of integers, $len$, $x, i$ are integer-valued variables, and $r$ is a Boolean-valued variable. I have to provide a loop invariant (using ...
2
votes
0answers
40 views

kPDA handling multiple epsilon transtions

I'm assigned to build a kPDA with 2 stacks that handles {w#w, where w is a string of (0,1)*}. I understand the # delineates the two strings, but I'm unsure of the logic when popping off stacks with ...
1
vote
2answers
106 views

What are the other language models of computation similar to lambda calculus?

I hope this question makes sense, but I was wondering if there are other models of computation similar to lambda calculus that you can use to build up axiomatic mathematical and logical fundamentals ...
5
votes
2answers
2k views

Why do ¬, ∀ and ∃ have the same precedence?

I thought the order of precedence of operators and quantifiers was arbitrary, but I don't really understand why those three have the same "strength" in relation to other operators (e.g., ¬ will have ...
1
vote
0answers
243 views

How do I get the NAND gate configuration for full adder from the logic table?

I'm self-studying, but I've gotten stuck already. If I'm given the logic table for a full-adder or any two-output table, how do I figure out the NAND-gate configuration, preferably methodically? ...
1
vote
0answers
53 views

Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode: ...
2
votes
1answer
368 views

Negation of the semantics of the Until operator in LTL

I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to: $\phi R \psi \equiv \neg(\neg\phi U \neg \psi)...
1
vote
1answer
42 views

Turing Machine where branches are resolved via arbitrary operator

Alternating Turing Machines output Boolean values and combine the values returned by branches via the any/all operators. Is ...

1 2
3
4 5
16