Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
166
questions with no upvoted or accepted answers
12
votes
1answer
540 views
The difference between dynamic logic and temporal logic
To find the difference, I'd just encountered with assertions below about temporal logic in Wikipedia:
another variant of modal logic sharing many common features with
dynamic logic, differs from ...
10
votes
0answers
330 views
Is Agda sound as a proof system?
I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's ...
7
votes
0answers
127 views
Boolean formula that agrees with most truth assignments
Let $X_1,\dots,X_n$ be $n$ boolean variables. I have an unknown predicate $P(X_1,\dots,X_n)$ on these boolean variables. Of course, I can view the predicate as a function $f_P : \{0,1\}^n \to \{0,1\}...
6
votes
0answers
176 views
On the Turing Completeness of First Order Logic
It is well known that in Descriptive Complexity Theory FO is equivalent to AC0.
However, this accepts a couple of a theory and a string <T,s> iff the ...
5
votes
0answers
33 views
Do FOL theorem provers accept axiom schemata?
Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata?
I looked in the Vampire "manual" briefly,...
5
votes
1answer
97 views
proving program equivalence
I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there ...
5
votes
0answers
134 views
Characterization of alpha-equivalence in languages with bindings
Following up on this post denoting $(x \leftrightarrow y)$ the permutation of $x$ and $y$ and $P[x \leftrightarrow y]$ the term obtained from the term $P$ by permuting $x$ and $y$ (so for example if $...
5
votes
2answers
231 views
propositional Modal logic filtration definition
Hello I have a slightly unusual question which relates to a definition of filtration structure. The following is my current state of the definition:
$ \mathcal{M} = (W, R, L) $, W is a set of worlds,
...
4
votes
0answers
194 views
Can every sentence of first-order logic be converted into an equisatisfiable equation in Boolean algebra?
There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational ...
4
votes
0answers
154 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
...
4
votes
0answers
48 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 ...
4
votes
0answers
45 views
Modern presentation of Ackermann's “Solvable Cases?”
Ackermann's book "Solvable Cases of the Decision Problem" discusses decidable instances of first order logic, particularly monadic logic, and so called "equality formulas". However, the book is from ...
4
votes
0answers
38 views
Quantum algorithms for logical inference - reference request?
Microsoft is committed to the building of the scalable, industrial size topological quantum computer, Visual Studio integrated programming language and SDK will be released by the end of this year (...
4
votes
0answers
67 views
What is the role of abstract machines in the Curry-Howard isomorphism?
By abstract machines I mean things like the SECD machine, Krivine's machine or more generally machines with states/memory/registers/stack/accumulator...
According to Wikipedia page of the Curry-...
4
votes
0answers
73 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 ...
3
votes
0answers
42 views
What's the average number of transistor switches needed to do an N-bit x N-bit multiply?
I want to know how switch-efficient a multiplier can be. If I need to do many $N$-bit by $N$-bit multiplies, and each bit is determined by flipping a coin, what's the average number of transistor ...
3
votes
0answers
68 views
Understanding $\lambda \mu$-calculus in more programming way
I am learning $\lambda \mu$-calculus (self-study).
I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
3
votes
0answers
39 views
conversion of basic $\text{CTL}^*$ formulas to $\text{CTL}$
Consider the $\text{CTL}^*$ formula $E[pU(qUr)]$.
It is not hard to show that it is equivalent to the $\text{CTL}$ formula $E[pU(EqUr)]$.
The informal reason is that a path where $p$ is true until $...
3
votes
0answers
72 views
An instance when you can eliminate propositional double negation in coq
Suppose st: string -> nat and X stands for the string 'X'.
Given the hypothesis ...
3
votes
0answers
56 views
A book introducing proof theory needed (many-sorted FOL, classical non-Gentzen calculus, satisfiability in partial algebras, induction)
We define a signature as a triple $$\Sigma\ =\ (S,F,\mathrm{type})$$ where $S$ is a set of sorts, $F$ a set of $n$-ary function symbols $f$ of the type $\mathrm{type}(f)$ $=$ $(M_1,\dotsc,M_n\...
3
votes
0answers
50 views
Expressing definite clauses (Horn rules, logic programming) in lambda terms?
There is paper which expresses lambda terms in the terms of logic programming http://www.cse.unt.edu/~tarau/teaching/PL/docs/dbx.pdf Is there conversion in the other direction - expressing definite ...
3
votes
0answers
144 views
Semantic parsing with Grammatical Framework - is this possible?
So far I have learned about categorial grammars, type logical grammars and formal semantics of natural language, the relevant tools are Cornell Semantic Parsing Framework https://github.com/clic-lab/...
3
votes
0answers
40 views
Sorts and constructors for modelling classes in a theorem prover
I have been working in the Welder theorem prover for some time now. But I'm confused in the way they handle data-types. I'm not familiar with the terminology of sorts and constructors. Here is how one ...
3
votes
0answers
55 views
How to express modalities in rule bases, knowledge bases or expert systems?
Knowledge bases and expert systems are usually production rules systems and as such they lack expressive means for expressing modalities like "agent believes in statement", "agent has duty to perform ...
3
votes
0answers
79 views
In ontology development, where do axioms come from?
I am developing an ontology. I've got the classes, relationships and I guess I could come up with instances at this point too.
But what I'm really focused on is the axioms. I've learnt that the ...
3
votes
0answers
35 views
What is example of Kahr formula $[\forall\exists\forall, (\omega, 1), (0)]$ and what to do if such undecidable formula is encountered in practice?
There are mentioned many classes of undecidable formulas in the book "The Classical decision problem" http://www.springer.com/la/book/9783540423249. Kahr formulae is one class of undecidable formuls ...
3
votes
0answers
70 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 ...
3
votes
0answers
268 views
Has someone seen this structure before?
I am working 1 with a certain structure,
and I wonder if someone has seen it before.
I am no mathematician, so all I can say is that
I will do my best to describe this structure.
It is actually very ...
3
votes
0answers
94 views
Spot the formalism (some kind of process logic)
Consider the following specification technique.
A specification consists of a finite set of triples $\langle C, A, C' \rangle$,
where $A$ is the name of an action and $C, C'$ are conditions, that is,
...
3
votes
3answers
569 views
Does exist any horn formula that is equisatisfiable to the clause that is disjunction of two literals? Does also exist equivalent?
I just and simply want to know if whether or not exist any horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to know if there also exists equivalent.
2
votes
0answers
34 views
Is there a diagram of related logics?
Proving software is based on logics and there any many logics. AFAIK all of the logics can be shown as a tree diagram of how they are related; for example, a tree of how types of number are releated
...
2
votes
1answer
25 views
Clarifying the definition of reduction with regards to NP-complete problems
In my logic class we started learning about the different complexity classes. In particular, we focused on the NP complexity class. A problem is in NP if it is solvable in polynomial time using a ...
2
votes
0answers
304 views
Prove that PRE-WORK-POST is Turing Complete
This is a homework question and I am trying to fully understand what I have to do and how to go about it. Therefore, I don't want full answers to the question.
The programming language PRE-WORK-POST ...
2
votes
0answers
22 views
Automated algorithm design
There is a huge field of study dedicated to automated theorem proving. Is there any similar research dedicated to automated algorithm design? And is there any form of "duality" between these ...
2
votes
0answers
33 views
Name for a function on formulae that does not break the structure of given formula
I have two logics, $L_1$ and $L_2$, and a mapping $f: Formulas_{L1} \rightarrow Formulas_{L2}$, and want to argue that the mapping is "nice", in the sense that it is structure-preserving. ...
2
votes
0answers
44 views
Can HOL be simulated in the CiC?
I was wondering if HOL (higher-order logic) can be simulated in the Calculus of Inductive constructions (CiC)
2
votes
0answers
32 views
Compiling an impure language into a pure stack-based language
For a personal learning and fun project, I build an abstract virtual machine based on a stack. The instructions are simple and act on the top of the stack only. There are also stack operators such as <...
2
votes
0answers
48 views
Large Conjunctive Normal Form Examples
I'm currently learning about conjunctive normal form in a course on logic for Computer Science. I was reading the Wikipedia entry on the subject and encountered this:
Typical problems in this case ...
2
votes
1answer
64 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
65 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 ...
2
votes
0answers
28 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 ...
2
votes
0answers
23 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 ...
2
votes
0answers
223 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 ...
2
votes
0answers
28 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 ...
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 ...
2
votes
0answers
137 views
Second Order QBF
Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first ...
2
votes
0answers
35 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 ...
2
votes
0answers
105 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
40 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 ...
2
votes
0answers
31 views
Superposition calculus: greater vs greater-or-equal
Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, ...
