# Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

110 questions
271 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 ...
118 views

37 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 ...
32 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 (...
61 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-...
30 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 ...
26 views

58 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) ...
44 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 ...
114 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 ...
31 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 ...
266 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 ...
92 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, ...
42 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 ...
34 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 ...
38 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 ...
39 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 ...
144 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 ...
97 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 ...
51 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 ...
89 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, ...
179 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, ...
86 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,...
87 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 ...
98 views

45 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 ...
114 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 "...
34 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 ...
27 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 ...
59 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 ...
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 ...
57 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, ...
210 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 ...
37 views

### Algorithm for deducing values

I have a group of logical conditions and need to deduce values that would NOT satisfy them. For example: City != New York && Location = Museum ...
29 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 ...
62 views

### Law as a computer science problem?

For a long time, computer scientists and logicians have noticed that law (statutes, contracts, adjudication, etc), has some similarity with formal logic and programming languages, and have approached ...
49 views

### What is this weird gate?

This came from a picture of something that I'm supposed to make, and I can't find it in the program I'm supposed to use (LogicWorks). It looks like it 'not's only one of its inputs, but that doesn't ...
30 views

### How do I get the NAND gate configuration for full adder from the logic table?

I'm self-studying, but I've gotten stuck already. If I'm given the logic table for a full-adder or any two-output table, how do I figure out the NAND-gate configuration, preferably methodically? ...
40 views

### Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?

I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode: ...
32 views

### Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?

As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
19 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, ...
34 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’...
45 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 ...