Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
709
questions
0
votes
0answers
6 views
Observational Determinism using HyperPCTL
I've found no material on HyperPCTL, so if you know please help me.
This is the definition of Observational Determinism expressed using HyperPCTL and i have some questions.
$\forall \sigma \, \forall ...
0
votes
1answer
12 views
What can't guarded fragment of FO express?
I have some basic confusions about the definition of the guarded fragment of first-order logic. Hopefully someone can tell me where I'm wrong.
GF in FO is defined by:
Atomic formulas, $x=y$ and $R(...
1
vote
2answers
56 views
Is there a formal definition for iteration?
I wanted know if there is a formal definition of iteration. In the sense that, this definition will say that after the 4th iteration is termination or the 5th iteration and not the 2nd iteration. ...
0
votes
0answers
27 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
438 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
50 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
48 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
40 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
111 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
39 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
89 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
84 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
144 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
61 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
42 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
41 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
84 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 ...
0
votes
1answer
27 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
66 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
57 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 ...
1
vote
0answers
31 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 ...
0
votes
0answers
13 views
Logical inference as Markov decision process?
Are there efforts to consider forward or backward (theorem proving) logical inference process as Markov decision process in which the the action space is: 1) selection of the inference rule (e.g. from ...
1
vote
1answer
43 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
33 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 ...
0
votes
0answers
17 views
Why does the unbounded $\mu$ operator preserve effective computability?
Let $f$ be a partial function from $\mathbb{N}^{p+1}$ to $\mathbb{N}$. The partial function $(x_1,...,x_p)\mapsto \mu y[f(x_1,...,x_p,y)=0]$ is defined in the following way:
If there exists at least ...
3
votes
0answers
31 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
33 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
47 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
47 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
1answer
52 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
36 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
65 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
49 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
208 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
39 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
31 views
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
45 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
48 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
91 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 \...
0
votes
1answer
38 views
What is the minimun 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
22 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
83 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
46 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
37 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
27 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
0answers
27 views
Handling $AND$ and $OR$ cases in MILP?
Suppose I want to have an integer program for handling the cases
$x_1>1\wedge x_2>1\wedge x_3>1\wedge\dots\wedge x_n>1\iff\delta=1$
$x_1>1\vee x_2>1\vee x_3>1\vee\dots\vee x_n&...
0
votes
1answer
53 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
59 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
34 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 ...
