K-user mailing list

[Everett Hildenbrandt <hildenb2 AT illinois.edu>]

Hey Zans,

If you are interested in equational logic, you'll probably need to do a lot of
unification and/or matching. The [Logik
language](https://github.com/kframework/k/tree/master/k-distribution/tutorial/2_languages/4_logik)
has an example of a Prolog-like language which demonstrates using unification.

In K we use two logics for reasoning, Matching Logic and Reachability Logic.
Matching Logic is an expressive first-order many-sorted logic with reflective
reasoning, making it suitable as a logical framework (roughly "a logic for
defining other logics in"). If your equational theory is expressible as a
confluent and terminating set of oriented rewrite rules, you may be able to
express it directly in K (without having to build a reasoning engine in K
itself). Look at [the FSL publications
page](http://fsl.cs.illinois.edu/index.php/FSL_Publications) for the papers on
reachability logic and matching logic for more information.

For inspiration, you may look at our prototype [Matching Logic
prover](https://github.com/kframework/matching-logic-prover) in Maude. Maude
definitions and K definitions can be (roughly) translated back-and-forth.

Let me know if you have more questions.

Everett H.

On Sun, Feb 05, 2017 at 10:17:26PM +0000, Park, Daejun wrote:
> Hi Zans,
> 
> Sorry for the delay in replying. Currently, we do not provide a nice 
> interface
> to express an arbitrary logic. We are actively working on fully supporting
> Matching logic (the underlying logic of K), in which you may be able to 
> embed
> your logic if possible.
> 
> Best,
> Daejun
> 
> On Jan 23, 2017, at 7:37 AM, Zans Mihejevs 
> <zans.lancs AT googlemail.com>
>  wrote:
> 
> 
> 
>     Hi, I've seen a few tutorials on implementing languages in K, but I am
>     struggling to find any explanation on how to express a logic.
> 
>     Would anyone have any suggestions? I am currently interested in 
> equational
>     and predicate logics.
> 
>