Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
751
questions
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 (...
-1
votes
0answers
22 views
what are the semantics of logic gates for non-binary system?
what are the semantics of logic gates for a non-binary system (decimal system)?
for example NOT gate semantic (for decimal) could be(x)= abs(x-9)
NOT(6)=3
what about for AND and OR gates, what are ...
0
votes
0answers
17 views
What could be the bound of the number of elements of a models of a given first order 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 ...
0
votes
0answers
28 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
126 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
21 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
64 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
194 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
138 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
16 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
31 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
69 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
23 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
54 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
23 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
46 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
143 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
46 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
39 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
21 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
40 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 ...
7
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
40 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
14 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
65 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
19 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
44 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 ...
2
votes
2answers
31 views
How to show all false outputs in a circuit?
I have 3 input variables and the output for all 8 possible combinations is 0 (false). When making a circuit, how would I show this using gates or no gates at all? Thanks!
1
vote
1answer
52 views
Can someone explain the logic diagram for the Boolean expression NOT A OR B AND C
An IB question requests:
Construct the logic diagram for the Boolean expression NOT A OR B AND C.
The answer
looks to me like not A or (B and C), whereas what I expected only gets partial credit. ...
5
votes
2answers
225 views
checking '<' for two binary numbers in a cnf-formula
I want to check whether a arbitrary binary number is less or equal to another binary number in a cnf-formula. I can already construct a formula, which is not in cnf:
Lets say n and m are two-digit ...
0
votes
0answers
36 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
11 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 ...
3
votes
1answer
49 views
How to Implement a reversible OR operator with a Fredkin gate (controlled swap)?
How to implement a reversible OR operator with a Fredkin gate ?
0
votes
1answer
32 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
39 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
28 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
68 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
42 views
prove that {$↔,⊕$} is incomplete set?
How do i prove that Is {$↔,⊕$} not a complete set ? I have no clue how to prove it .
3
votes
1answer
107 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
32 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
89 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
16 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
22 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
68 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
32 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
469 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
58 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 ...
