Skip to content

Incorrect grounding of formula with two bi-implications. #12

Open

Description

@GoogleCodeExporter
What steps will reproduce the problem?

1. Using the attached MLN and evidence file, run:

     $ infer -i net.mln -e evidence.db -q R -outputNetwork -r ground.lcnf

What is the expected output? What do you see instead?

The input cnf has a formula of the form:

A <=> (B <=> C).

The grounded formula should give us constraints of the form:

!A v !B v C.
!A v B v !C.
A v !B v !C.
A v B v C.

Instead, it gives us an unsatisfiable formula consisting solely of unit clauses.

What version of the product are you using? On what operating system?

January 2013 release. Linux, Fedora 20, x86_64.

Please provide any additional information below.


Original issue reported on code.google.com by Kopp.Ti...@gmail.com on 10 Feb 2015 at 4:44

Attachments:

Activity

  1. GoogleCodeExporter commented on Dec 3, 2015

    @GoogleCodeExporter
    Author
    Nevermind, upon closer inspection it _is_ being grounded correctly.
    

    Original comment by Kopp.Ti...@gmail.com on 10 Feb 2015 at 6:03

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions