Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
1
vote
0answers
24 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
votes
0answers
26 views
Is it possible to do forward-chaining in Prolog?
Prolog (or any logic programming system) actually acts as SAT solver, that returns the valid values for the variables that are mentioned in the query. It can also be used as theorem prover if one does ...
0
votes
0answers
11 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
28 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
32 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
30 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
32 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
45 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
39 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
46 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
26 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
61 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
48 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
202 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
34 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
42 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
36 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
38 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
81 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
35 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 ...
0
votes
1answer
20 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
57 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
42 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
33 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
25 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
0answers
35 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
39 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 ...
1
vote
2answers
79 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
30 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
39 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
82 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
35 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
vote
2answers
62 views
If a NAND gate is universal, why you don't have NAND OISCs
If a NAND gate can be used to construct all other of the basic logic gates, then I'm wondering why you don't/can't have a purely NAND-based One Instruction Set Computer (OISC). All the OISC single ...
0
votes
0answers
36 views
Can we see all of mathematics as an attempt to simplify computations?
This is a rather strong claim, and therefore likely to be incorrect, but hear me out.
Firstly, when I talk of “computations”, I mean this in a broader sense than normally used, because I am including ...
1
vote
2answers
43 views
(Generally) How to specify asynchronous action with side effects using logic equations
Say you have this function call sequence:
function all() {
fn1()
fn2()
fn3()
}
And say that fn2 was asynchronous and ...
2
votes
1answer
38 views
Examples of logic gates using non-standard models
These are the only ones I have been able to find online:
Pulley Logic Gates
Marble adding machine
MARBLE COMPUTER LOGICAL AND GATE
I would like to find some more discrete models like these (as ...
0
votes
1answer
52 views
LTL to Büchi automaton, deterministic?
I know it is possible to convert LTL formulas to Büchi automatons. But is it possible to convert a LTL formula to a deterministic Büchi automaton? Are there formulas that can't be converted to a ...
2
votes
1answer
22 views
How to understand the notion of boolean query via Immerman's definition
A query is any mapping $I:STRUC[\sigma] \to STRUC[\tau]$ that is polynomially bounded. A boolean query is a map $I_b: STRUC[\sigma] \to \{0,1\}$. A boolean query can also be thought as the susbset:
$...
3
votes
2answers
102 views
Interesting logic problems
I've just began a course on logic and learned the following :
De Morgan's laws
Normal forms
How to represent a logical formula (using or, and, not operators) using binary trees
How to ...
1
vote
2answers
81 views
D flip flop : How does it work in depth
I'm coming to you today because I have some trouble to understand how works D flip flop in depth. Two weeks ago we started at school learning sequential logic and so register and everything that come ...
5
votes
2answers
60 views
Topology vs sigma-algebra's as a framework for approximate information?
In the book "topology via logic" by Steven Vickers, topology is introduced for computer scientists, with the idea that topology captures the idea of approximate information.
I am somewhat confused ...
2
votes
1answer
152 views
Decidability of equivalence to existential formulas
I'm looking for an algorithm to decide if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are ...
0
votes
1answer
42 views
How to evaluate dynamical conditioning/pseudo code
I am having a hard time even to formulate my question, so here it is:
I have an application that the user can go in and define on a webpage the logic one wants to evaluate for the student to comply ...
1
vote
1answer
58 views
What is the signature of a formal language?
I will briefly state the context where my doubts arise.
I know the following definitions.
A formal language is a set of well-formed formulas. It's a tuple constituited by an alphabet and a formal ...
0
votes
0answers
29 views
Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?
As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
