Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

10
votes
0answers
242 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 ...
6
votes
0answers
116 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
146 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
119 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 $...
4
votes
0answers
36 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
27 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
59 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
71 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 ...
4
votes
0answers
30 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
17 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
39 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
41 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

Finiteness of the set of equivalence classes of formulas generated by boolean combination

Define a relation $\equiv$ on the set of modal formulas by $\phi \equiv \psi \Leftrightarrow (\forall M\forall w, M,w \models \phi\Leftrightarrow M,w \models \psi)$ (so it is an equivalence relation) ...
3
votes
0answers
38 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
73 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
63 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, ...
3
votes
0answers
39 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
64 views

Construct skolemform of: $\forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X, S,T))$

This question is not asking for a solution, but rather as a check / validation of my thought process. Given the form: $W = \forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X,...
3
votes
0answers
43 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
112 views

Higher order verification in a complete logic

I'd like to design a language that is able to reason over itseslf, means, able to get as input a code in that language (that might have went through some external redundant preprocessing, or "...
3
votes
0answers
263 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
90 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, ...
2
votes
0answers
112 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
95 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
50 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
160 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
71 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
68 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
95 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) $...
2
votes
0answers
33 views

physical significance of membership function greater than one

In fuzzy logic, when we associate an element with a set, we usually do it in terms of membership grade which suggests the "belonging" of this element to the set. Membership grade value 0 means that ...
2
votes
0answers
25 views

BDI logic or KARO framework solver - are there solvers for any new logic?

I am reading about agent logics and especially affective agents. There are BDI logics and combination of logics called KARO framework that considers those questions. All those logics seem to be ...
2
votes
0answers
57 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 ...
2
votes
0answers
48 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
0answers
56 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
0answers
192 views

Difference between fully-reduced BDD and quasi-reduced BDD

I am trying to figure out difference between fully- and quasi-reduced BDDs. I have read a lot of material but still it is not very clear. As I am trying to figure out the quasi reduced version for ...
1
vote
0answers
23 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 ...
1
vote
0answers
22 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 ...
1
vote
0answers
16 views

Propositional extentionality in the lean theorem prover?

Propositional extentionality in the lean theorem prover is stated as the following axiom: axiom proptext {a b : Prop} : (a $\iff$ b) \to a = b My confusion about this is as follows: Previously I’...
1
vote
0answers
28 views

Type theory based automated theorem prover?

I know that there exist type theory based proof-checker, and I know that there are logic/sequent-calculus based automated theorem provers. But I haven’t heard of a type-theory based automated theorem ...
1
vote
0answers
26 views

How to minimize large DNF formula into deeper but smaller formula?

I want to minimize DNF formula which has ~200k products combined into a sum. The depth of that formula is 2 - first level is the OR, and second level is AND for all conjunctions. I have tried using ...
1
vote
0answers
59 views

Difference between logic, fuzzy logic, probabilistic logic, quantum logic?

I am not sure if the names of these logics are right, but I saw that you can generalize logic with probability theory. Then I found 3 ways of reasoning with probabilistic/smooth logic, Fuzzy, Bayes/...
1
vote
0answers
21 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 ...
1
vote
0answers
39 views

Understanding a Single Step in the Model Checking Algorithm

This answer explains roughly how to convert a nested boolean function into a Binary Decision Diagram (BDD). This question is about how to structure the states for the BDD. Now in this question I am ...
1
vote
0answers
30 views

How to apply Hoare Logic to this function

I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to ...
1
vote
0answers
45 views

What is the definition of the property of Canonicity for a logic?

I'm trying to understand "A Systematic Approach to Canonicity in the Classical Sequent Calculus" by Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. The article discusses a property called "canonicity" ...
1
vote
0answers
23 views

how to use the solution of mean payoff game to arrive at winning regions of parity game?

The 7th chapter (7.3 section) of "Automata Logics and Infinite Games" by Erich Gradel, Wolfgang Thomas, Thomas Wilke gives a way to convert max parity game to mean payoff game. I do not understand ...
1
vote
0answers
49 views

Hoare correctness proof for a recursive definition of multiplication

Given the program: {y=y0 ^ y>=0} z=0; while (y>0){ z=z+x; (1) y=y-1; } {z=x*y0} I am having trouble finding the ...
1
vote
0answers
16 views

Subsymbolic/multimedia knowledge - query, creation and reasoning? Reference request?

One can consider multimedia data as a matrix of pixels, but, of course - multimedia data contains higher-order knowledge as well. E.g. everyone can describe famous paintings in terms of colours, ...
1
vote
0answers
37 views

Unable to have an equivalent of A(FG p) and AG(EF p)

It states in my lecture notes that there is no CTL formula that is equivalent to A(FG p) in LTL and likewise, there is no LTL formula that is equivalent to CTL formula AG(EF p). I am just starting to ...
1
vote
0answers
51 views

Universal theorem proving algorithms for sequent calculus (e.g. for cut-free logics)?

Some of the logics admit Gentzen-style sequent calculus. Are there universal algorithms that allow to find proof (derivation of the proof) in sequent caculus for every hypthetical theorem? Some of ...