# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

166 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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 ...
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 ...
127 views

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, ...
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 ...
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 ...
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 ...
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 ...
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 (...
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-...
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 ...
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 ...
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 ...
39 views

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 ...
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/...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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, ...
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.
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 ...
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 ...
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 ...
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 ...
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. ...
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)
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 <...
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 ...
64 views