proj-oot-ootLogicNotes1

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/

---

trellis and prolog both could usee an assertion/truth maintanence syntax

---

---

https://www.fpcomplete.com/school/to-infinity-and-beyond/pick-of-the-week/a-little-lens-starter-tutorial#-sidenote--what-is-that-forall-thing-- 's forall:

" >>> view _1 ("goal", "chaff") "goal"

>>> forall $ \tuple -> view _1 tuple == fst tuple True "

forall is being used here as a form of an assertion; it's an assertion with a variable in it

---

Ceptre: A Language for Modeling Generative Interactive Systems.

Ceptre: A Language for Modeling Generative Interactive Systems. Chris Martens 2015

    We present a rule specification language called Ceptre, intended to enable rapid prototyping for experimental game mechanics, especially in domains that depend on procedural generation and multi-agent simulation.
    Ceptre can be viewed as an explication of a new methodology for understanding games based on linear logic, a formal logic concerned with resource usage. We present a correspondence between gameplay and proof search in linear logic, building on prior work on generating narratives. In Ceptre, we introduce the ability to add interactivity selectively into a generative model, enabling inspection of intermediate states for debugging and exploration as well as a means of play.
    We claim that this methodology can support game designers and researchers in designing, anaylzing, and debugging the core systems of their work in generative, multi-agent gameplay. To support this claim, we provide two case studies implemented in Ceptre, one from interactive narrative and one from a strategy-like domain.

Some choice quotes from the artice follow.

Simple examples of the rule language:

    The meaning of A -o B, to a first approximation, is that whenever the predicates in A are present, they may be replaced with B. One example of a rule is:
    do/compliment:
         at C L * at C’ L * likes C C’
      -o at C L * at C’ L * likes C C’ * likes C’ C.
    [...]
    Note that because of the replacement semantics of the rule, we need to reiterate everything on the right-hand side of the -o that we don’t want to disappear, such as the character locations and original likes fact. We use the syntactic sugar of prepending $ to anything intended not to be removed in order to reduce this redundancy:
    do/compliment: $at C L * $at C’ L * $likes C C’ -o likes C’ C.
    A more complex rule describes a murder action, using the ! operator to indicate a permanent state:
    do/murder:
        anger C C’ * anger C C’ * anger C C’ * anger C C’
        * $at C L * at C’ L * $has C weapon
      -o !dead C’.
    (This rule consumes C’s location, maintaining a global invariant that each character is mutually exclusively at a location or !dead.) Here we see a departure from planning formalisms: four instances of anger C C’ mean something different from one. Here we are using an emotion not just as a precondition but as a resource, where if we have enough of it, we can exchange it for a drastic consequence. Whether or not we diffuse the anger, or choose to keep it by prepending $ to the predicates, is an authorial choice.

Concurrency in narration:

    Two rule applications that consume disjoint sets of resources from the same state can be said to happen concurrently, or independently. On the other hand, a rule that produces resources and another that consumes a subset of them can be said to be in a causal, or dependent, relationship. Less abstractly, if resources represent facts associated with particular game entities or characters, then independent rule applications represent potentially concurrent action by multiple such entities, and causally related rule applications represent either sequential action by a single actor, or synchronized interaction between two entities.

Stages, and a larger example:

    We would like to for some of these rules to run automatically without player intervention. In our next iteration of the program, we will make use of a Ceptre feature called stages. Stages are a way of structuring a program in terms of independent components. Syntactically, a stage is a curly-brace-delimited set of rules with an associated name. Semantically, a stage is a unit of computation that runs to quiescence, i.e. no more rules are able to fire, at which point control may be transfered to another stage.
    [...]
    Additionally, we can test the design by “scripting” certain player strategies. For instance, we could augment the two rules in the fight stage to be deterministic, fighting when the monster can’t kill us in one turn and fleeing otherwise:
    stage fight = {
      do_fight:
          choice * $fight_in_progress * $monster Size * $health HP * Size < HP
        -o try_fight.
      do_flee :
          choice * fight_in_progress * $monster Size * $health HP * Size >= HP
        -o flee_screen.
    }
    If we remove interactivity from this stage, then we get automated combat sequences that should never result in the player’s death.

By gasche at 2015-08-04 14:03

Logic/Declarative login or register to post comments other blogs 2504 reads

---

we need some language to express guarantees: eventual, C,A,P, atleastonce, atmostonce, A,C,I,D, B,A,S,E, ordered (and all these with rspect to certain operations or classes of ops, eg availability wrt read ops but not wrritee ops; i guess capabilities can use the same ops descr language), guaranteed, best-effort, permitted/forbidden required/optional, deterministic/stochastic, before/after/during, known/unknown are these alphanumeric identifier prefixed with a sigil that means "<ome sort of modal logical thing"? mb "?" is the sigil?

---

note: sigi uses 'connection words' "and, does, has, is" in http://communitywiki.org/en/nLSD. That's a nice set of beginning 'predicate' like things.

note: unlike has, is, does, sigi's connection word 'and' is being used not so much as an ordinary relation (which is like a clause, i guess; "Bob is blue"), but rather to create a noun phrase, which is like a struct

---

todo: check out https://en.wikipedia.org/wiki/Common_Logic

http://www.jfsowa.com/talks/clintro.pdf also describes the IKL (Interoperable Knowledge Language) extension to Common Logic, which Sowa seems to like (more on IKL: http://www.ihmc.us/users/phayes/IKL/GUIDE/GUIDE.html http://philebus.tamu.edu/cl/docs/cl/SemTech2008/Menzel-SemTech2008.pdf http://philebus.tamu.edu/cl/docs/cl/SemTech2008/cl_sowa.pdf

http://www.iso-commonlogic.org/

also i've already looked into it a bit, but "topic maps" should be noted, for later readers

note: Common Logic is a later version/offshoot of KIF https://en.wikipedia.org/wiki/Knowledge_Interchange_Format

---

need to distinguish 'is' into:

and we also need modals for:

eg :

---

sometime look into "conceptual graphs" too

maybe also look into Murray Altheim (from CW)'s project, Ceryle (which seems to have been deleted, but here's some of the docs): http://web.archive.org/web/20081029023001/http://altheim.4java.ca/ceryle/wiki/Wiki.jsp?page=UserDocumentation

unfortunately i cant seem to find copies of his ontologies: http://web.archive.org/web/20070321051852/http://altheim.4java.ca/ceryle/wiki/Wiki.jsp?page=CeryleOntologies . The docs site for Ceryle is down and the SourceForge?