ideas-computer-jasper-jasperLogicNotes1

I guess if we are doing 'RDFt' we should generalize this to add other modifiers (qualifiers and quantitiers, but other stuff too, i guess) to RDF, e.g. certainty level, provenance/source of evidence, mode, scope (time and place at which the assertion is made; these are like propositional phrases in English i guess), forall/exists,exactlyone, etc. Consider adding the other Kantian categories too. Hmm, that generalization is pretty interesting...

mb call this idea 'RDF+'

the tinkerpop guys are already onto 'RDFt': http://nosql.mypopescu.com/post/21377687732/distributed-temporal-graph-database-using-datomic

--

and of course we need the ontological basics too.. can start with looking at semweb stuff like OWL (and RDF and N3) and topic maps

--

need a syntax to encompass most logics e.g. most deductive inference systems, as well as the basics of proof theory, model theory

e.g. a general framework for definining logic programming languages like Prolog or constraint satisfaction languages

--

is the benefit o RDFt over traditional data structures obtainable by adding roles to datastructures and autoconverting, e.g. homomorphisms?

--

http://en.wikipedia.org/wiki/Refal ( http://en.wikipedia.org/wiki/Markov_algorithm )

--

to look into:

--

www.ksl.stanford.edu/people/stolle/Papers/meta96.ps

adds control clauses to prolog to allow programmer to control order of goal selection during theorem proving

--

" Metaprolog..the extensions are primarily aimed at allowing programs to manipulate multiple theories, allowing distinct theories to have multiple 'viewpoints' of a relation, and to make proofs available as terms in the language' "

"Reflective Prolog...allows the programmer to extend the object-level provability relation by clauses to be used at the metalevel. However, a Reflective Prolog program is an amalgamated theory (bayle note: i think they mean that the object level assertions and the metalevel assertions live in the same space), containing object level axioms as well as metalevel axioms. For example, the clauses

solve(#P($X, $Y)) :- reflexive(#P), solve(#P($Y, $X)). reflexive(<spouse>).

(where #P is a metalevel variable ranging over names of predicate symbols while $X and $Y are metalevel variables ranging over names of terms) say that a binary atom, whose predicate symbol denotes a reflexive relation, can be proved by instead proving an atom whose arguments have been exchanged with respect to the original atom; the predicate 'spouse' denotes such a relation "

the Godel language has metaprogramming modules for datatypes representing Godel programs and theories, and also predicates that attempt to prove a formula

MOL (i didnt understand this part)

Meta by Kowalski... name each theory by opaque terms that do not themselves indicate the axioms for that theory.. but you can give those separately.

Combinatory Logic Programming... makes for more efficient implementations

Truth predicates "Sato "Metaprogramming through a truth predicate" has investigated the use of a self-referential truth predicate, given semantics in three-valued logic, for metaprogramming. Jiang "on the semantics of real metalogic programming.. advocates a language with a nonground representation that does not distinguish between terms and sentences.."

Alloy "combines ideas from Reflective Prolog (automatic meta-to-object reflection as an inference rule) and Kowalski's Meta (the representation of theories and the application of meta-to-object reflection also to program clauses)."

so, 3 uses of metaprogramming in logic (Barklund counts 4 but i identify 2 of his): writing/extending compilers etc; controlling procedural behavior; representing/reasoning about knowledge

Barklund speaks a lot about how it is problematic to use 'improper nonground representations', in metalogic, that is, representations in the metalanguage of expressions in the base language which contain metavariables, because there is "a high risk that the programmer introduces subtle errors by unintentional instantiation of metavariables that actually represent object variables". i don't understand this, too bad Barklund didn't give examples.

-- Metaprogramming in Logic by J Barklund - ‎1994 - CiteSeerX? citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.52.2769

---

https://en.wikipedia.org/wiki/Answer_set_programming

--

upvote

mafribe 13 hours ago

link

Neither Coq nor Isabelle are based on Martin-Löf Type Theory (in a narrow sense). Coq is based on a variant of the calculus of construction (with (co)inductive definitions) and Isabelle is an LCF-style prover framework that you can instantiate with various different logics. The most widely used variant is Isabelle/HOL which implements a variant of Church's theory of types. To implement other logics, Isabelle uses intuitionistic second order logic based on lambda calculus, without numbers or recursive data types. Idris has Type:Type, so is unsound as a logic. I'm not sure exactly what Epigram uses, but I assume it's somehow based on Luo's ECC. Only Agda is based on Martin-Löf Type Theory.

reply

upvote

tel 12 hours ago

link

Yeah... This is correct as far as I know though a bit out of my complete technical grasp. To my understanding MLTT was a fairly central topic and it helps to distinguish MLTT from just type theory since plain-old-TT might be harder to distinguish as something interesting above `(int *)`.

But, to solidify, mafribe is much more correct than my comment and there's, as far as I'm aware, a much larger menagerie of other type theories. The recent Homotopy Type Theory publication—which was on HN as notable due to its publication process—was yet another step in this direction.

reply

--

hmm.. even if you use relevance logic instead of the material conditional, you give up truth-functionality but you still have some other stuff:

---

probabalistic programming:

http://en.wikipedia.org/wiki/Probabilistic_programming_language

http://probabilistic-programming.org/wiki/Home

http://radar.oreilly.com/2013/04/probabilistic-programming.html

https://projects.csail.mit.edu/church/wiki/Church

http://probcomp.csail.mit.edu/venture/

http://probabilistic-programming.org/wiki/NIPS*2012_Workshop

http://probcomp.csail.mit.edu/bayesdb/