Questions related to mathematical logic and its use in computer science

learn more… | top users | synonyms (1)

2
votes
0answers
28 views

Z into Isabelle

I am trying to input and prove Z specifications in Isabelle. Say I have a vending machine specification written in the LaTeX format: ...
-1
votes
1answer
44 views

Why decision problem definition ignores Gödel incompleteness theorem?

The following question assume that the decision problem definition (syntactic) has been written (and could be changed if it isn't able) to catch a concept (meaning, semantic) which has both nice ...
0
votes
1answer
34 views

Rewriting gates such as XOR into three basic gates? [closed]

How would I rewrite an XOR gate into the three basic logic gates (AND, OR, NOT). To be more specific, I have to write it in such a way with 2 NOT gates, 2 OR gates, and 1 AND gate. I also have to do ...
0
votes
2answers
29 views

Operator precedence in propositional logic

there is some kind of priorities for the elements in propositional logic ? for example : p ∧¬q → r , given this ,we there may be two options (p ∧¬q) → r OR p ∧ (¬q → r) , which one is the correct ...
2
votes
3answers
147 views

How to construct XOR gate using only 4 NAND gate?

XOR gate, now I need to construct this gate using only 4 NAND gate ...
3
votes
1answer
27 views

Extended version of the theory of reals and its decidability

It is well-known due to Tarski that the theory of reals $(\mathbb{R},+,\cdot,<,=)$ is decidable. I was asking my self whether one would lose the decidability by adding all real constants. More ...
8
votes
2answers
77 views

Assignment to make formula unsatisfiable

Lets imagine we have a satisfiable formula $F(A_0, A_1,...A_k,S_0,...,S_n)$ The problem to solve is "Is there an assignment for variables $(S_0,...,S_n)$ which will make F unsatisfiable?". One way of ...
1
vote
1answer
88 views

Intuition behind F-algebra

I looked at here for getting an intuition about F-algebra, but I am still left with some questions. Suppose I have a group signature as $\Sigma= (* : X \times X \rightarrow X, \thicksim: X ...
2
votes
0answers
24 views

Parameterized complexity of Weighted Satisfiability with few variable occurrences

Given an integer $k$ and a Boolean CNF Formula $\phi$, Weighted Satisfiability asks whether $\phi$ is satisfiable by a model of weight $k$, i.e., a model that sets at most $k$ variables to true. This ...
1
vote
1answer
52 views

m-functions in Turing's paper “On Computable Numbers and applications…”

I was reading Alan Turing's paper "On Computable Numbers with an Application to the Entscheidungsproblem". I was reading well until I encountered "4. Abbreviated Tables", page 235-236, where Turing ...
2
votes
1answer
41 views

Formalizing self-propagating behaviour

Since reading Ken Thompson's Reflections on Trusting Trust I am trying to formalize the idea of a program which mutates its own behaviour; specifically, a program that would be self-reproducing except ...
2
votes
1answer
32 views

If in all satisfying assignments all pair of variables can take all possible values is this tautology?

I suppose this is both easy and false. Let $\phi$ be propositional boolean formula on variables $x_1 \ldots x_n$. Suppose in all satisfying assignments of $\phi$, all pairs of variables $(x_i,x_j),i ...
2
votes
1answer
29 views

Undecidable definition of pure function?

I am trying to come up with a formal definition for functional purity in a simple programming language (think JavaScript). What I've got so far is this: DEFINITION: A statement is impure if ...
3
votes
1answer
36 views

What is the rigorous definition of an efficient algorithm that $\epsilon-refutes$ random 3CNF formulas

I recently asked a similar What does "refuting random 3CNF" formulas mean?, however, I'd like to address it in a more mathematically precise setting. In that paper, on page 5, it talks ...
0
votes
0answers
16 views

What is the exact difference between kripke structures and transition systems?

Depending on the exact definition of a kripke structure and a transition system, they seem to be pretty much the same thing - is this true? To be more specific - though i found differing definitions ...
3
votes
2answers
66 views

What does “refuting random 3CNF” formulas mean?

Intuitively, recall what 3CNF formulas mean: Its a boolean formula with conjunctive normal form (i.e. formula of ANDs of clauses with ORs) with no more than three variables per conjunct. I was ...
1
vote
1answer
19 views

Are there two kinds of polynomial hierarchy collapses?

It seems to me that there are two different situations which get called ``PH collapse", (1) That $\exists i \geq 1$ s.t $\Sigma_i ^p = \Sigma_{i+1}^p$ (2) That $\exists i \geq 1$ s.t $\Sigma_i^p = ...
1
vote
2answers
47 views

Curry Howard correspondence and Church-Turing thesis

Curry-Howard correspondence states the equivalence between logic/deduction and types/programs. The Church-Turing thesis states the equivalence of some models of computation. Specifically, all ...
4
votes
1answer
320 views

Why is automated theorem proving impossible?

As far I know, in general case there is no Turing machine which could get any theorem on its input and produce its proof on its output. Why is it so?
5
votes
4answers
96 views

Can I use ellipses in first order logic

I ask, because I have to come up with a first-order logic sentence that shows that there are exactly N objects in the universe. What I've been able to come up with is: $$ \forall x \; \exists y_1, ...
3
votes
3answers
192 views

How was the ALU implemented in the first computer (i.e., Babbage's analytical engine)?

I've seen circuit level implementations of ALU's before, but how are NOT/AND/ADD performed mechanically?
0
votes
1answer
70 views

Given a set of LTL formulas, on which states does the Kripke structure hold? [closed]

I'm currently learning about LTL and CTL formulas and to get a better understanding I try to manually interpret the formulas over a given Kripke structure. Since I'm not 100% sure if my results are ...
0
votes
0answers
74 views

Algorithm for scheduling timetable for student management system

I am developing the timetable module for a student management system. I am finding it difficult to design/develop it. It can be assumed that a given teacher is capable of teaching any standard whether ...
-1
votes
1answer
24 views

Digital Logic Settle Time

I have an exam tonight and I'm reviewing my midterm exam. I got this question completely wrong, with no solution given. ...
1
vote
0answers
18 views

Efficiently decidable logics

So propositional logic (PL) is efficiently (in P) decidable because I can convert formulas to an equisatisifiable CNF-formula, negate and convert (efficiently, by De Morgans laws) to DNF. I can then ...
1
vote
2answers
57 views

The use of modal logic in computer science [closed]

I have a tentative understanding of modal logic. Can anyone explain modal logic as it is used in computer science?
7
votes
1answer
343 views

DNF to CNF conversion: Easy or Hard

In relation to the thread CNF to DNF — conversion is NP Hard (and a related Math thread): How about the other direction, from DNF to CNF? Is it easy or hard? On Page 2 of this paper, they seem to ...
-2
votes
1answer
78 views

A logic function that is true iff the first operand is less than the second operand

In my computer organization class I have been given a series of problems. One I'm stuck on currently is below: Assume that $X$ consists of 4 bits, $x_3 x_2 x_1 x_0$, and $Y$ consists of 4 bits, ...
0
votes
1answer
52 views

If $F$ is valid then $F \cup \{res(C_1,C_2,A_i)\}$ is valid

I have to prove the following problem in propositional logic: Let $F$ be a set of clauses and let $F' = F \cup \{res(C_1,C_2,A_i)\}$ be the extension of $F$ by a resolvent of some clauses $C_1,C_2 ...
2
votes
1answer
87 views

Abstract algebra and programming languages

Quite often, I stumble upon abstract algebra concepts like initial algebra, free algebra, and similar while reading papers on programming languages. For instance, in papers on algebraic data types, ...
0
votes
1answer
87 views

Finding a Hoare logic correctness proof for a Repeat-Until loop

How can we prove a program in repeat until using Hoare Logic? I've found a rule like this: {P} S {R}, {R ^ ~B -> P}, {R ^ B -> Q} for ...
3
votes
2answers
84 views

Skolemization with multiple arguments — how to unify

Edit: answerers keep finding (valid!) problems with my example. I'll try again. The older version is below the horizontal line. Thanks to Klaus below for pointing out the last problem. My ...
6
votes
2answers
121 views

What do we gain by having “dependent types”?

I thought I understood dependent typing (DT) properly, but the answer to this question: Why was there a need for Martin-Löf to create intuitionistic type theory? has had me thinking otherwise. ...
0
votes
0answers
32 views

Solving Subproblem in Logic (first-order, propositional, pddl)

One sentence question Is there any algorithm able to prove (solve) a logic problem (first-order, propositional, pddl) by finite induction? Background I am researching Hierarchical planning solvers ...
3
votes
1answer
223 views

What's the purpose of ANDing a bit mask with all bits set to a value?

I'm adapting an algorithm for calculating a CRC 16-bit CCITT (XModem) value from an ASCII input. I've found some code here. I'm using the function the poster has in his question, but I've noticed at ...
1
vote
1answer
24 views

Unification — removing equations and updating the solution

This question is concerned with the first order unification. Suppose I have a set $D$ of equations and a solution to these equations. Let this solution be a set $S$ of substitutions. Now, suppose I ...
0
votes
3answers
189 views

Combinational Logic - Need help with proof by rewrite

In my Computer Logic class we were assigned the following problem: Complete a truth table that has $3$ inputs $(A, B,C)$ and one output $(F)$. $F$ is asserted whenever $B$ or $C$ are ...
3
votes
1answer
49 views

Can a propositional threshold connective be expressed by standard connectives?

We are given a finite set of propositional atoms $\{x_1, \dots, x_n\}$ and an integer $k$. Can we capture through a propositional formula $\varphi$ (built from the standard connectives $\neg, \wedge, ...
2
votes
2answers
70 views

Logical Reduction

Reducing one computable problem to another by providing an algorithm which transforms an instance of one problem to one of the other (and limiting the time or space of that algorithm) is clear to me. ...
1
vote
1answer
70 views

CTL - model checking for formula $A [a \cup b]$

I'm trying to verify if the following model satisfy $A [a \cup b]$: The algorithm I'm using is taken from "Concepts, Algorithms, and Tools for Model Checking", Joost-Pieter Katoen. In particular I ...
2
votes
0answers
34 views

What are the fundamental principles/algorithms on the process of equation solving?

I have seen a lot of solvers that are capable of, for example, getting an equation such as x ^ 2 + x = 12 and finding x = [3, -4]. I know some of them are implemented by hardcoding special cases. For ...
2
votes
1answer
71 views

CTL vs LTL - when a formula satisfy a model

I'm trying to understand the difference between LTL and CTL. In particular, i'm trying to understand when a model (a transition system eg. Kripke structure) satisfy a formula. This is my point of ...
-1
votes
2answers
112 views

Show this is a tautology without using a truth table

I am doing a homework assignment and I've been stuck on this question for a long time now. The question says to prove this equation is a tautology without using a truth table. I assume we have to use ...
0
votes
1answer
53 views

Defining a new operator in CTL

Lets consider a new operator $B$ where $a B b$ means "in every execution, if $b$ holds some time, then $a$ does so before it" and we're asked to define it in CTL. My working: the system can only ...
1
vote
0answers
47 views

Formulating an arrangement problem with STRIPS

The problem is rearranging furniture in a flat. We are given rectangular rooms of natural width and height with doors between them, (the walls have no width) and rectangular furniture at starting ...
0
votes
1answer
54 views

Defining a new (informal) operator in CTL

If you were given a "new operator" Wh and a formula a Wh b meaning that a holds for at least as long as b does (in all executions). How would you define this operator in CTL? This is an exercise ...
0
votes
3answers
53 views

Simplifying a boolean expression

I need to prove: XY+~XZ+YZ=XY+~XZ I cannot think how to do this. I have tried factorising, but I just don't know of any rule that removes one of the terms like above. I start with the LHS, ...
1
vote
2answers
120 views

Some slight confusion with the UNTIL operator in CTL (e.g. a U b)

I've sketched a very small transition system in paint that I'll use as an example. I want to see if $A(aUb)$ holds for this transition system. From my understanding, this CTL formula is asking if ...
2
votes
2answers
188 views

Is Karnaugh Map possible for Maxterms?

I read about Minterms i.e. sums of products, simplification using Karnaugh Graph. Can this graph be used for Maxterms, i.e. products of sums, as well? If yes, then how? If not, then is there some ...
0
votes
1answer
56 views

Given this transition system, for which states are these (very basic) LTL formulas fulfilled?

I missed a lot of lectures for this module due to surgery so I'm trying to teach it to myself now. This is the question I've been working on: First of all, would I be correct in saying that the LTL ...