Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
153
questions with no upvoted or accepted answers
12
votes
1answer
516 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
318 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
126 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
167 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
1answer
89 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
212 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
145 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
44 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
43 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
34 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
64 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-...
3
votes
0answers
32 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
64 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
49 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
139 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
78 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
34 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
65 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
531 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
56 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 ...
2
votes
0answers
30 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
34 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
48 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
55 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
22 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
218 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
26 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
134 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
95 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
30 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, ...
2
votes
0answers
85 views
Why Modus ponens works with Horn clauses and Generalized Modus ponens requires definite clauses?
I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward ...
2
votes
0answers
49 views
Unification algorithm that directly finds multiple substitutions?
Systems of formal logic generally have inference rules that
require certain expressions to be syntactically the same
in multiple steps. Typically two steps are involved, as
for modus ponens, where ...
2
votes
0answers
24 views
Is it possible to define logic programming for every logic that has implication and conjunction connectives?
Is it possible to define logic programming for every logic that has implication and conjunction connectives? Does logic programming adds something new to the usual inference process. By usual ...
2
votes
0answers
195 views
Equivalence preserving operator from CTL* to LTL
The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
2
votes
0answers
101 views
Is there an analysis of the creation of axioms for a mathematical structure as a computational problem?
Historically, what has happened is the following:
There is a "mechanical" structure, most importantly, arithmetic, which operates according to a set of well-defined rules that a stupid computer can ...
2
votes
0answers
54 views
Automatic learning/discovery of logics
Are there efforts to automatically discover new logics? Logics are simple structures - they have formal language, deduction rules, semantics and certain properties that are proved or discarded for ...
2
votes
0answers
131 views
Passing arrays vs functions as arguments in SMT?
In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions.
In the theory of arrays, ...
2
votes
0answers
199 views
Recursive definitions, How it is done?
I read that recursive definitions, refer to the definition of a function in that function body, cannot be done in $\lambda$-calculus, but recursion can be achieved by using $Y$ combinator.
As I know, ...
2
votes
0answers
107 views
Unification algorithm - need clarification
I have these two terms:
{P(a,x,x),P(a,b,c)}
I'm supposed to find if the terms and unifiable using the unification algorithm.
I'd do the following substitutions:
b/x, resulting in : {P(a,b,b),P(a,b,...
2
votes
0answers
92 views
How to know whether a formula is common knowledge in Kripke structure?
Suppose that we have a formula A which is valid in all states of Kripke structure and some transition relations. Is it generally possible to derive if formula A is common knowledge between particular ...
2
votes
0answers
99 views
Satisfying of $\square (\neg A \cup B)$
Let's consider the following formula:
$\square (\neg A \cup B)$.
Does the following computation satisfy it?
The numbers in brackets are number of state.
(0) $\neg A, \neg B$
(1) $\neg A, B$
(2) $...
