Boolean¶

A Boolean extension of ASP.

Usage¶

Run the test instance in examples/bool/tests/and_not.test.lp with the following command:

> metasp solve clingo examples/bool/tests/and_not.test.lp --meta-config examples/bool/config.yml
Metasp (<class 'metasp.app.ClingoApp'>) version 5.8.0
Reading from examples/bool/tests/and_not.test.lp
Solving...
Answer: 1 (Time: 0.165s)
c
a
SATISFIABLE

Models       : 1+
Calls        : 1
Time         : 0.165s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.153s

UI¶

metasp ui examples/bool/tests/and_not.test.lp --meta-config examples/bool/config.yml

Example¶

Simple example

{b}.
{a}.
&not(&not(a)).

Definition of the system¶

Configuration¶

syntax-encoding:
  - "./syntax.lp"
semantics-encoding:
  - "./semantics.lp"
printer: pretty_printer

Syntax¶

#type bool{
    expressions: {
        &not/1 : {
            type: bool, safety: unsafe;};
        &and/2 : {
            type: bool, safety: safe;
            type: bool, safety: safe;};
        &or/2 : {
            type: bool, safety: unsafe;
            type: bool, safety: unsafe;};
        &to/2 : {
            type: bool, safety: unsafe;
            type: bool, safety: unsafe;};
    };
    subtypes:  { atom; };
    occurrence: any;
    macros:   {
        &eq(f1, f2): &and(&to(f1,f2), &to(f2,f1));
        where: { f1: bool; f2: bool; };
    };
}.

Semantics¶

Uses the provided standard encodings:

meta.lp for the meta predicates.
show.lp for the show predicates.
reify-defined.lp to avoid warnings for the reification predicates.

`semantics.lp` ¶

Encoding

#include "metasp.show.lp".
#include "metasp.meta.lp".
#include "metasp.reify-defined.lp".
#include "metasp.reify-defined-metasp.lp".

Not¶

:- formula(bool, &not(F)), true(&not(F)), not not true(F).
true(&not(F))   :- formula(bool, &not(F)), not true(F).

And¶

true(&and(F1,F2)) :- formula(bool, &and(F1,F2)), true(F1), true(F2).
true(F1):-true(&and(F1,F2)).
true(F2):-true(&and(F1,F2)).

Or¶

true(&or(F1,F2)) :- formula(bool, &or(F1,F2)), true(F1).
true(&or(F1,F2)) :- formula(bool, &or(F1,F2)), true(F2).
true(F1);true(F2):-true(&or(F1,F2)).

To¶

true(&to(F1,F2)) :- formula(bool, &to(F1,F2)), true(F2): true(F1).
true(F2) :- true(&to(F1,F2)), true(F1).

Warnings¶

Checks and warnings to showcase logging from ASP

has_not(&not(F)) :- formula(bool, &not(F)).
_log(warning, nested_negation(&not(F))):- formula(bool, &not(F)), has_not(F).