Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
770
questions
1
vote
0answers
14 views
How is it possible that an equational theory be terminating?
I'm a bit tripped up by this fundamental notion of an equational theory with respect to how we can possibly get termination if we have that we can always orient a set of equations either right to left ...
1
vote
1answer
17 views
Injectivity not required for unification algorithms?
When learning about a general unification algorithm, we learned the rule decompose, which states unifying
$$G \cup \{f(a_0,...a_k)=f(b_0,...,b_k)\} \Rightarrow G \cup \{a_0=b_0,...a_k=b_k\}.$$
The ...
1
vote
1answer
18 views
Why does the substitution {x/f(y), y/z} work this way?
There is an example of applying a substitution to an expression, and I am having a problem with it.
Let $\theta = \{ x/f(y), y/z \}$, and $E=p(x,y,g(z))$,
then $E\theta = p( f(y),z,g(z) )$.
Why is $...
2
votes
1answer
25 views
Definition of 2-CNF (a.k.a Krom) formula
In my lecturer's notes, the following definition for a 2-CNF wff is given:
A 2-CNF formula, or Krom formula is a CNF formula F such that every clause has at most two literals.
However, there is ...
1
vote
0answers
22 views
Logic minimization via 2 inputs NOR gates: Is it monotone w.r.t to adding a minterm?
notation: $x+y:=\mbox{OR}(x,y)$, $\bar x:=\mbox{NOT}(x)$, $xy:=\mbox{AND}(x,y)$, 1:=TRUE, 0:=FALSE.
Let $f$ be a Boolean function of $n$-variables, i.e. $f: \{0,1\}^n \to \{0,1\}$.
minterm:= any ...
2
votes
1answer
33 views
Natural deduction proof: distributivity of existential quantification
In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic:
$(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,...
2
votes
0answers
51 views
Sample applications based on First Order Logic
I often hear about benefits of FOL, but I wonder what are some of its real world applications?
Could someone please provide samples/case studies of applications of FOL that address real world ...
1
vote
0answers
21 views
Is Event Calculus applied for program verification?
Recently I've read wiki page about Robert Kowalski (Prolog author) and stumbled upon interesting concept of Event Calculus. The wiki article mentions only few applications of this logical language. I ...
1
vote
1answer
27 views
What is Herbrand interpreration and model?
I was reading the book "Foundations of Logic Programming" written by J.W. Lloyd. In the book, there were definitions of interpretation and model, and when it comes to herbrand interpretation and model,...
0
votes
0answers
26 views
Prove that exists PARITYn fuction with size O(n^2)
Have to find Boolean circuit formula that solves PARITYn problem with complexity O(n^2)?
(Function PARITYn(x1, . . . , xn) is equal to 1 if and only if the number of variables x1, . . . , xn equal ...
5
votes
1answer
82 views
How come correctness proofs aren't tautological?
Consider the following function on binary trees, which is supposed to tell whether a given int is a member of a binary tree t:
<...
0
votes
1answer
34 views
Representing a sentence using propositional logic
I am confused regarding a propositional logic representation of a sentence.
Please note that this sentence is not realistic:
"A person who is male (M) is smart (S) if he is tall (T), but otherwise ...
0
votes
0answers
51 views
How to show that a partial function is recursive?
I try to prove that this function is recursive:
$$f(x_1,x_2)= \begin{cases}
2x_1-x_2 & \text{if $x_1 \geqslant \sqrt{x_2}$} \newline
\bot & \text{otherwise}
\end{cases}$$
I think that I need ...
1
vote
0answers
14 views
Is true * true = true in Separation Logic?
I am trying to show that the following interference is unsound in terms of Separation Logic:
$$
(p_0 \implies p_1) \implies ((p_0 * q) \implies (p_1 * q))
$$
I came up with the following values for ...
1
vote
1answer
39 views
What algorithms for unification over (multidimensional) array terms?
I am looking for references on implementing unification over multidimensional array terms.
Are there specialized unification algorithms for those cases? I wasn't able to find satisfactory literature ...
2
votes
2answers
55 views
Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$
I am new to LTL and I am trying to understand how it works. My question is: is there such $\sigma$ that:
$ \sigma \models [\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)]$
I know ...
0
votes
0answers
28 views
Formalizing “dual-time” temporal logic
I am interested in modeling a discrete temporal logic based on music, where there are two metrics of time, beat and seconds, (call them B and S). The constraints on what constitutes a syntactically ...
1
vote
0answers
72 views
Proving a first order logic theorem in equational logic with a term rewriting system
I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean ...
0
votes
0answers
21 views
In what sense the computer program (Turing machine) can be considered as the complex system and its IIT Phi can be measured and improved?
I am reading https://global.oup.com/academic/product/a-world-beyond-physics-9780190871338?cc=us&lang=en& about one approach of complex systems' theory for the emergence of the life. It is ...
2
votes
0answers
21 views
Deciding Intuitionistic Logic via QBF
I want an algorithm to decide whether a theorem holds in propositional Intuitionistic logic ($IL$). We know $IL$ is $PSPACE$-complete, so we should be able to reduce $IL$ to $QBF$.
In Literature i ...
0
votes
2answers
163 views
Does the callback concept of programming have any basis in computer science?
Although I seriously code with computer languages in general since 2010 and as an amateur programmer with programming languages in particular since 2015 (primarily Bash and JavaScript imperative ...
0
votes
0answers
11 views
Synthesis of the crisp programs from the Bayesian (probabilistic) programs?
https://arxiv.org/abs/2001.00805 is the article which is pointing towards the direction that the optimal policy of the reinforcement learning can be expressed as the Bayesian/probabilistic program (...
0
votes
0answers
26 views
Bounds on the size of the universe of a model for an FO-sentence
Sorry for the weird title.
The Problem:
Consider the first-order logic sentence
φ≡∃s∃t∃u∀v∀w∀x∀yψ(s,t,u,v,w,x,y) where ψ(s,t,u,v,w,x,y,) is a
quantifier-free first-order logic formula using ...
1
vote
0answers
32 views
Proof strategy to show that an algorithm cannot be implemented using just hereditarily terminating procedures
I am taking my question here from there. Consider the following scenario:
You are given a fixed programming language with no nonlocal control flow constructs. In particular, the language does not ...
0
votes
0answers
14 views
Is the standard terminology “logic operation” or “logical operation”?
I've heard both terms "logic operation" or "logical operation" used. Is either more common?
2
votes
1answer
134 views
Is it possible to prove Tarski's Undefinability theorem from Turing's Halting Problem?
In the Wikipedia page for Turing's Halting problem, they mention that you can prove Gödel's First Incompleteness theorem from it. This is the relevant quote:
Assume that we have a sound (and hence ...
1
vote
1answer
24 views
Simplifying a logic function using Boolean algebra
Consider this Logic function : D = A B C + A B’ C + A’ B’ C + A B C’ + A’ B C’ + A B’ C’ I am trying to simplify it using Boolean algebra , I am stuck in this step : D= AB +B'C+ A’ B C’ + A B’ C’ So ...
2
votes
2answers
68 views
diagonal lemma and the negation function
Carnap's diagonal lemma asserts that for every computable formula f, accepting a natural number as argument and resolving to {false,true}, there exists a logic sentence s for which:
s $\...
3
votes
2answers
239 views
Why is the assignment rule the way it is in Hoare Logic?
Why is the assignment rule the way it is in Hoare Logic/Axiomatic Semantics?
I can't wrap my head around why the assignment rule is backwards from what I expected.
I understand Hoare logic is use to ...
2
votes
0answers
211 views
Given undirected and connected graph G=(V,E). Prove for any DFS run: for any u,v∈V if u.d>v.d then u.d−v.d≥δ(u,v)
Given undirected and connected graph $G = (V,E)$.
Prove for any DFS run: for any $u,v \in V$ if $u.d>v.d$ then $u.d − v.d ≥ δ(u,v)$
$δ(u,v)$-distance of a shortest path (not necessarily unique) in ...
0
votes
0answers
17 views
Proving the existence of a $\Pi_1$-sentence in True Arithmetic that is independent of Peano Arithmetic
I am trying to wrap my head around how to prove the following statement:
There exists some $\Pi_1$-sentence $A$ such that $A \in \textbf{TA}$ but $\{A, \neg A\} \cap \textbf{PA} = \emptyset$.
$\...
1
vote
2answers
34 views
Are these two sensible and related or unrelated ways of regarding a logic system as a programming language?
When I am trying to understand logic programming languages e.g. Prolog, I am immediately confused by the following two ways of relating logic systems and programming languages or type systems.
In ...
4
votes
1answer
70 views
Is there a model of ZF¬C where some program always terminates but has no loop variant?
Wikipedia has a proof that every loop that terminates has a loop variant—a well-founded relation on the state space such that each iteration of the loop results in a state that is less than the ...
2
votes
0answers
25 views
How to prove following two statements are equivalent in Hilbert System?
statement 1: $Γ$ is satisfiable implies $Γ$ is consistent.
statement 2: If $Γ$ derives $α$ then $Γ$ entails $α$.
I can easily prove statement 1 from 2 , but not 2 from 1 (without using strong ...
1
vote
1answer
55 views
Meaning of $a\lor b \to b' \lor c'$
So I have done part a) but I have no clue what I am supposed to do for part b), I have been trying for days to wrap my head around and even asked my fellow course mates, none of which seem to know ...
1
vote
1answer
28 views
Simplification of a multi-index Boolean expression towards computation in fewer steps
Let $x_{ij} \in \{0,1\}$, $1 \leq i \leq M$ (typically, $M = 2000$), $1 \leq j \leq N$ (typically, $N = 10$), be Boolean variables. If possible at all, I would like to simplify the following ...
1
vote
1answer
48 views
General resolution in first order logic
Assuming you have a formula in first order logic like
$$(\forall_x p(x) \land \forall_x q(x)) \rightarrow \forall_x(p(x) \land q(x))$$
(which seems valid?)
Converting the formula to ...
3
votes
3answers
148 views
Are regular languages and their regular expressions part of computer science?
I am trying to understand if regular languages and their regular expressions are concepts of computer science in general and if these are discovered, or invented, by computer scientists, in particular....
0
votes
0answers
47 views
On the complexity of existential and universal quantifiers
I'm trying to analyze the time complexities of the two former kind of quantifiers, I need help figuring out if I'm following the right path or if I'm making mistakes, here's what I've produced so far:
...
4
votes
1answer
40 views
Is unification over regular expression equations doable?
By way of example, suppose I know that $X + a = b + Y$ where $X$ and $Y$ are variables standing for regular expressions, then $(X, Y) = (b, a)$ is a solution to this set of equations.
Generalizing ...
1
vote
1answer
25 views
What does it mean when a dot appears in a logic gate other than the NOT gate? (in logic diagrams)
For example, this gate:
looks like an OR gate, except there's a dot to the right. The dot is reminiscent of the fact that there's a dot in the NOT gate, so I wonder if it has something to do with ...
3
votes
1answer
46 views
Combining Predicate Logic and BigO
I am a beginner to predicate logic and BigO and am having though time understanding the definition of BigO in terms of predicate logic in the picture attached. I particularly am unable to understand ...
8
votes
2answers
2k views
Language to define perfectly a programming problem
Is there any language, which can be used to define all programming problems perfectly?
By perfectly, I mean with these two properties:
p is the problem.
d is the definition in the language.
P(d, p): ...
2
votes
1answer
54 views
Addition, multiplication, and apostrophe used to represent boolean algebra expressions?
I'm looking at a worksheet that expresses boolean logic expressions using multiplication, addition, and apostrophes; something I've never seen before.
I can make a guess that the apostrophe is ...
0
votes
0answers
15 views
How to compute (partial) consequence set for premises of the first order logic?
I am playing with the Sequent Calculus Trainer https://www.uni-kassel.de/eecs/fachgebiete/fmv/projects/sequent-calculus-trainer.html . It is game with judgments, where each judgment consists from: 1) ...
1
vote
1answer
81 views
Can a dfa return only the final state?
I am given an assignment to design a tiny arithmetic unit (from 0 to 15 inclusive) start with 0 and using a DFA. The operations are as follow:
increment x+1 and if x+1 is larger than 15 then x+1 ...
2
votes
0answers
20 views
Determining Cumulative Benefit of Orders with Various Items
I'm working on a project to change the location of items in a warehouse to allow me to ship items together which were bought in the purchase order (currently impossible due to conveyor logistics). The ...
0
votes
0answers
54 views
Why do intuitionists accept the nonconstructive proof that the halting problem is undecidable? [duplicate]
On the intuitionism page at Stanford Encyclopedia of Philosophy (SEP), it's said in Section 3.3 that
Because of the finiteness of a natural number in contrast to, for example, a real number, many ...
0
votes
2answers
57 views
Why there is forward chaining inference engine (reasoner) for description logics only and not for other logics?
Reasoner is forward chaining inference engine (https://en.wikipedia.org/wiki/Semantic_reasoner) as opposite to Prolog backward chaining SAT solver (for queries). Why there is reasoner for description ...
1
vote
1answer
34 views
Complexity of negation cancellation
Consider propositional logic over the connectives $\land$, $\lor$, and $\lnot$. Notation: $| \alpha |$ is the length of formula $\alpha$.
We are given a formula $\phi$. Cancel all cancellable ...
