# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

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

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

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 ...
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/...
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 ...
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 ...
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 ...
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 ...
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, ...
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.
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 ...
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 <...