# Tag Info

12

When I say "von Neumann architecture", I mean some hardware that is limited by the "von Neumann bottleneck" -- i.e., it has all data is funneled through some narrow data bus. The non-von Neumann programming languages I bump into most often are VHDL and Verilog. In VHDL and Verilog, by default, everything happens at the same time. The programmer has to go to ...

11

I will just write what Frank Pfenning taught me (all mistakes go on my account). A traditional formal system in logic, such as natural deduction, is descriptive in the sense that it tells us what valid deductions are, but it does not tell us how we are supposed to look for them. The starting point of logic programming is to take the rules of deduction and ...

11

I assume by non-Von Neumann, you mean languages that bypassed the "Von Neumann Bottleneck" as per Backus' paper "Can Programming Be Liberated from the Von Neumann Style?". For those interested, you can find a copy here: http://www.thocp.net/biographies/papers/backus_turingaward_lecture.pdf The answer to your question will have to be ambiguous for a few ...

8

FO-LFP is neither complete (its valid sentences cannot be described by a recursively presented proof system) nor compact (there is an unsatisfiable set of sentences all of whose finite subsets are satisfiable). The basic argument is given in Denis’s answer so I won’t repeat it here, but let me instead point out that as a general principle due to Per ...

6

Any logic defined semantically in a similar way is trivially consistent, as it has a model. Any finite-valued logic has a faithful translation into classical logic, hence its set of valid formulas, or even the consequence relation, are recursively enumerable. Completeness is a relationship between semantics and a proof system. You only gave the semantics, ...

5

Let's assume that your three-valued logic consists of the truth values Yes, No and "unknown". We can think of these truth values as the sets $\{\top\}, \{\bot\}, \{\top,\bot\}$, and then the logical operations result in all possible values. For example, Yes and Unknown is Unknown while No and Unknown is No. A trick known as "double rail logic" uses two ...

5

You should have a look at Uniform Proofs as a Foudation for Logic Programming by Dale Miller, Gopalan Nadathur, Frank Pfenning and Andre Scedrov, 1991. The idea of this work and the rich area that has seen spawn from these ideas is to understand the execution of a logic program as proof search in simple and expressive logics, such as intuitionistic logic or ...

4

What do you mean by the equality in your first formula? In first-order logic (FOL) with equality, one can only apply the equality operator to a couple of terms, not to formulae. Also, your use of equality cannot be considered a case of definition (what could be better depicted by $\triangleq$) since the predicate List appears on both sides of the equality. ...

4

Prolog embodies the idea of computation as proof search. That is: a program is a formula which we would like to satisfy, the computation is the proof search, and the result is the witness for the formula. To make this idea work we need to reformulate the rules of first-order logic so that they can be read as instructions for execution of a proof search. We ...

3

Thank you for a great question! I am looking into papers on related subjects myself--I'll post anything worthwhile that I come across, and would appreciate if you would do the same. = ) Off the top of my head, you might be interested in ileanTAP, a Prolog theorem prover for intuitionistic logic (includes a short paper). Just so the term is not left undefined:...

2

It does not extend. Consider FO-LFP with just a binary predicate $<$, and the axioms for $<$ being a total order, with first and last positions, and every position has a successor. Moreover, we add an axiom saying that the last position can be reached from the first by iterating the successor function as a smallest fixpoint. This ensures that the ...

2

I think Linda and tuplespace programming could fit the bill. Associative/pattern matching memory operations with concurrency mean that (conceptually) the Von-Neuman bottleneck is eliminated. Going in that direction, a pure Actor-model languages also model communication rather than instruction sequencing. And although they are formalisms and not actual ...

2

Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty. ...

1

If your setting is FOL then why not just use a FOL theorem prover. What is unclear from your question is what you mean by general case. Using a FOL theorem prover covers any such query you could write in FOL... although of course, FOL is semi-decidable so it is not guaranteed that you can get an answer. Your problem can be written in the TPTP language as ...

1

What semantics of the logical operators would you like to have? Two of the best studied semantics for degrees are (propositional) Łukasiewicz logic and Gödel-Dummet logic. The latter enforces the domain to be a linear order which would allow you to model them via the naturals. It is also axiomatizable, since it is equivalent to intuitionistic propositional ...

1

Prolog deals with a formal system which is a small fragment of first order logic: it uses a logic of definite clauses, which are disjunctions of atoms and negated atoms, with the resolution rule as only inference rule. If you're not completely familiar to formal (logic) systems you just need to know that they are basically sets of rules: rules that ...

1

Not open source, but the AI engines of some successful computer games are based on modal logic, see e.g. "Using Exclusion Logic to Model Social Practices" and "Introducing Exclusion Logic as a Deontic Logic" by Richard Evans.

Only top voted, non community-wiki answers of a minimum length are eligible