Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
719
questions
0
votes
0answers
31 views
Did I prove the language is not regular?
I am trying to prove the following language that is not regular.
I used Pumping Lemma proof and my proof goes as follows:
Assume that L is regular and let p be the constant of Pumping-Lemma.
This ...
1
vote
0answers
8 views
Do forward chaining (Rete) business rules (Drools, ILOG) / production rules support higher order rules and compositionality?
There is this talk http://andrewcropper.com/pubs/jelia19-typed.pdf about higher order Prolog, about use of higher-order predicates (that takes other predicates as arguments) and compositionality of ...
0
votes
1answer
25 views
How to correctly negate a predicate bounded by some quantifiers?
this is a problem which was asked in GATE CS 2010.
This is question statement:
Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
0
votes
0answers
36 views
How to write negation of an 'AND' statement in logic
Suppose the given proposition is:
"Zach blocks emails and texts from Jennifer"
Where,
P implies "Zach blocks emails from Jennifer".
Q implies "Zach blocks texts from Jennifer".
So it's P AND Q in ...
0
votes
0answers
23 views
Are there lightweight logic of commonsense reasoning?
Logic generally is hard and probabilistic logic (with model counting, like ProbLog2) is even harder. But commonsense knowledge and reasoning is quite lightweight. There have been efforts to represent ...
3
votes
2answers
64 views
Euclidean Models
I am asked to prove that every Euclidean models satisfies $\diamond \diamond \diamond \varphi \to \diamond \diamond \varphi$. How can this be done? I don't see how it could even be true.
0
votes
2answers
34 views
prove that {$↔,⊕$} is incomplete set?
How do i prove that Is {$↔,⊕$} not a complete set ? I have no clue how to prove it .
-1
votes
0answers
25 views
Transforming Lambda Calculus syntax into generic relations between finite strings
I am trying to validate the simplest possibly notion of a formal system as relations between finite strings. I know that Lambda Calculus has the expressive power of a Turing Machine:
<λexp> ::= &...
3
votes
1answer
105 views
Are these 2 equivalent?
Is ∀x∀y∀z[φ(x,y)∧p(y,z)->p(x,z)] equivalent to ∀x∀y∀z[φ(x,y)∧p(x,z)->p(y,z)] ?
The only thing I can think of is that this question can be answered if we show that ...
0
votes
0answers
25 views
Mutually contradicting rules in Prolog
What will happen in a Prolog program, if I set two rules/facts which contradict each other..
will it go with the rule/fact that appears first.. or it will show an error?
4
votes
0answers
47 views
How shall I understand the definitions of `let` expression?
let as used in programming languages is defined in lambda calculus as per https://en.wikipedia.org/wiki/Let_expression#Let_definition_defined_from_lambda_calculus
...
0
votes
0answers
12 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
19 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(...
2
votes
2answers
65 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
29 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
454 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
52 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
57 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
41 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
120 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
103 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
88 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
148 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
64 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
43 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
45 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
91 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
34 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
69 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
49 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
36 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
18 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
32 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
48 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
49 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
55 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
41 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
214 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
44 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
46 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
49 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 ...
