Questions related to mathematical logic and its use in computer science

learn more… | top users | synonyms (1)

1
vote
1answer
35 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 ...
0
votes
0answers
16 views

How to solve a priority encoder truth table?

I am stuck in understanding the solution of the following problem. I wish to understand how one would start to solve it. I know the different truth table of each of the four operations but don't get ...
2
votes
0answers
30 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
32 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
3answers
83 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
47 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
38 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
49 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
47 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
68 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 ...
1
vote
1answer
23 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
34 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 ...
2
votes
3answers
50 views

Can someone clarify this unification algorithm?

I've been having trouble understanding a unification algorithm for first order logic, as I don't know what a compound expression is. I googled it, but found nothing relevant. I also don't know what a ...
1
vote
2answers
53 views

Turing Machine That Accepts Machines With Undecidable Languages

So I'm reviewing my Computability notes for my final, and I understand how reduction arguments work, but I'm having trouble framing one for the following Turing machine: Undecidable TM = { ⟨M⟩ | L(M) ...
1
vote
0answers
18 views

Open Standard Prolog Knowledge Bases [closed]

Are there any standard Prolog knowledge bases available anywhere that have the same purpose as Cyc, namely to encode generally accepted common sense and human knowledge? Typically containing ...
0
votes
1answer
35 views

Resolution refutation [closed]

This is an assignment so I don't want the answer, just maybe a push in the right direction. The question is: Suppose you are given an algorithm $R$ that can test for any propositional formula in ...
1
vote
0answers
16 views

SMT solves with functions for free varibles

So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions ...
1
vote
1answer
43 views

Is the extension of every undecidable theory undecidable?

While it is not the case that the extension of every decidable theory is decidable, is it true that: the extension of every undecidable theory undecidable? In other words, given an undecidable ...
3
votes
2answers
60 views

Underlying language to specify various types of logic

There exist several different types of logic -- 1st order, 2nd and higher order with many different sets of inference rules possible. What I'm having trouble understanding is what's the "underlying ...
2
votes
1answer
110 views

Is There a Programming Language That Embraces Globals?

All programming languages have globally defined symbols. While best practices invariably abjure their use as mutable entities the philosophy of what is mutable and what is not mutable is highly ...
3
votes
2answers
141 views

Free and bound variables

I am familiar with free and bound variables theory , but while learning I somewhere saw this lambda expression ((lambda var ((fn1 var) & (fn2 var))) argument) From what I have learned it ...
2
votes
0answers
30 views

Understanding a paper on polynomial recursion in all finite types

So I wasn't sure weather or not this counted as "research level" or not but I figured it wasn't so I decided to post it here. There is a paper by S. Bellantoni et al. called "Higher Type Recursion, ...
2
votes
1answer
217 views

Proving Linear Time Temporal Logic formula □ ◊ f ⇔ ◊ □ f

I am new to this topic, Linear Time Temporal Logic and I am trying to prove this equivalence -- $\Box\Diamond f \Leftrightarrow \Diamond\Box f$ This is my take -- Basic definitions: $(\sigma, j) ...
1
vote
1answer
45 views

Hamming Weight to find the sum of 1 bits in the range between A and B inclusive [closed]

I am trying to find the sum of 1 bits in the range between A and B inclusive, where -2^31 <= A <= B <= 2^31 - 1 Input Format: The first line contains the number of test cases T ...
0
votes
1answer
30 views

Type checking relation to logic

I am learning logic and functional programming and there is a topic called Type checking and their relationship to logic , I am unable to find any source that can help me in understanding this topic. ...
1
vote
2answers
43 views

Working out the connectives (And, Or, Not) in a Truth Table that has the outputs [duplicate]

I don't understand how to work backwards to work out a truth table that has been filled out already (I don't know the logical operators). E.g P | Q | Output 1 | 1 | 1 1 | 0 | 0 0 | 0 | 0 0 | 1 | 0 ...
0
votes
1answer
16 views

Prove the existence of a proposition logical formula so that following conditions are fulfilled

For two proposition logical formulas $\phi$ and $\chi$ so that $\phi\implies\chi$ is generally valid. How can I prove that there is a formular $\psi$ with $var(\psi )\subseteq var(\phi )\cap var(\chi ...
0
votes
0answers
22 views

Creating branch less than equals zero MIPS instruction in single cycle circuit

As a project I'm trying to implement a MIPS processor. I have a circuit similar to the one below. My question is what would be a way to implement a ...
6
votes
2answers
108 views

Does the Y combinator contradict the Curry-Howard correspondence?

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
0
votes
1answer
32 views

Karnaugh Map is this the simplest solution possible?

I'm learning to use a Karnaugh map but I'm not sure if I obtained the simplest expression possible. Have a look at this example Truth table (where A B C yield F): ...
0
votes
1answer
45 views

Difference between equivalence and implication

In terms of CTL formulae, what is the difference between equivalence and implication? (prop = some proposition, && = conjunction, AG = CTL syntax for "globally holds") E.g. AG (prop1 ...
1
vote
1answer
42 views

How can I translate this quantified logical expression into english

I was reading chapter-1 The Foundations: Logic and Proofs from this book. The chapter gives example of translating English sentence : "There is a woman who has taken a flight on every airline in the ...
-1
votes
1answer
31 views

Meaning of empty clause

Why does the empty clause is logically equivalent to a contraddiction: $\square \cup \square \Longleftrightarrow \perp$ and why the empty cube is logically equivalent to a tautology: $\square \cap ...
2
votes
1answer
22 views

Terminology about the word Function : General vs Computable

I've seen two different concepts referred to by the term "function": A small part of a program specified by the composition of constants and other functions as paramaters, such as the "functions" in ...
1
vote
2answers
34 views

Using the rules of inferences

I know the rules of inferences and logical equivalence but I cannot seem to validate this argument. I rewrote the first premise as $\neg p\vee q$ other from that I am stuck. Any help will be ...
2
votes
1answer
83 views

Computational equivalences between a calculus and an automaton model

This Wikipedia table (template for "Formal languages and grammars") maps grammar to language to abstract machine for more than a dozen languages. ...
0
votes
2answers
52 views

How can I simplify the following Product of Sums: ab+ac'+a'b'+a'c+b'c'+bc?

I started with POS: (a+b+c)(a+b'+c)(a'+b+c)(a'+b+c') and after a long while, I got: ab+ac'+a'b'+a'c+b'c'+bc and then I'm not sure how to simplify this. I thought maybe I can cancel the ab with a'b', ...
2
votes
1answer
107 views

Propositional logic — syntactical completeness

Lets consider propositional logic. We say a proof system for propositional logic is syntactically (negation) complete if for every $\alpha$, either $\alpha$ or $\neg \alpha$ are provable within the ...
4
votes
2answers
83 views

What is the definition of a $\Pi_1$-sentence?

What is meant when somebody says that a problem can be expressed as a $\Pi_1$-sentence? I know that for the arithmetical hierarchy, a $\Pi^0_1$-sentence is a sentence of the form $\forall n_1\forall ...
0
votes
1answer
38 views

Descriptive complexity: 3-colorability example

So in Neil Immerman's book http://books.google.co.kr/books?id=kWSZ0OWnupkC&pg=PA113&lpg=PA113#v=onepage&q&f=false, 3-colorability problem in descriptive complexity fashion is expressed ...
0
votes
2answers
49 views

Recursive equations vs. inference rules

It seems to me that recursive equations can always be presented as inference rules. For the forward direction, an example is addition over Peono numerals (built from $O$ and $S(\_)$) $$ ...
0
votes
3answers
42 views

A graph in descriptive complexity - is $x$ already a vertex?

So suppose that there is an undirected graph with edge connections known. Now in first-order logic there is quantifier $\forall x$. Then does this automatically refer to vertexes, or can we use ...
1
vote
1answer
51 views

How to prove that a predicate is prefix closed

Suppose we have the predicate $\qquad A.p.q ≡ (∀i \mid p≤i≤j<q : X.i≤X.j)$ which says that $X[p..q)$ is ascending. Apparently, the predicate holds for empty segments, is prefix closed and is ...
3
votes
3answers
425 views

Does a logical system have semantics?

From Wikipedia: A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to ...
2
votes
1answer
56 views

Does Herbrand's theorem mean any first-order logic formula can be expressed in CNF?

Herbrand's theorem shows that any formula of first-order logic can be expressed as a disjunction of quantifier-free formulas of first-order logic. Is this equivalent to saying that Herbrand's theorem ...
4
votes
1answer
44 views

First Order interpretation of arbitrary structures as a graph

I am currently trying to get some intuition on the concept of First Order reductions, and have come across this exercise question by Immerman, dubbed "Everything is a Graph". Given some arbitrary ...
-2
votes
2answers
95 views

Example for an unsatisfiable formula that can be made satisfiable by reordering quantifiers [closed]

Please give me an example of an unsatisfiable quantified 2 CNF formula. I need it in my proof and I am unable to think of one. I am looking for such an unsatisfiable quantified 2 CNF formula which ...
3
votes
1answer
76 views

Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?

Definition: A renamable Horn formula is a Boolean formula that can be transformed into a Horn formula by flipping the polarity of every instance of one of more of its variables. Example: $\qquad ...
0
votes
0answers
50 views

How to ascertain that the result of 1's complement arithmetic is invalid/valid

Trying to do (5)$_{10}$-(-5)$_{10}$ in 4 bit 1's complement system: 0101-1010 = 1011 with borrow 1 Subtracting back borrow 1011 - 1 = 1010 So sign bit is 1 in final answer, thus in 1's ...
-3
votes
1answer
46 views

Why is Mixed Quantified Horn SAT in PSPACE?

I want to prove that Mixed Quantified Horn SAT is a PSPACE-complete problem. I have proved that it is PSPACE-hard. How can I prove that it is in PSPACE? My study: To prove QSAT to be in PSPACE: ...