Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

AIC Seminar Series

Gen2sat: A Generic Tool for Reasoning with Non-classical Logics

Yoni ZoharTel Aviv University[Home Page]

Notice:  Hosted by Richard Waldinger

Date:  Thursday, August 24th 2017 at 4:00pm

Location:  EK255 (SRI E building)  (Directions)

Join Remotely: 

Available on VTC.

The wide adoption of modern SAT-solvers in industry and Academia has shown that propositional classical logic is a very powerful and useful tool. However, some aspects of reasoning, such as incomplete or imprecise information, are not representable in a natural way within classical logic, which led to the development of non-classical logics, such as constructive logics, many-valued logics, paraconsistent logics, and more.

While some of these logics are actually used in practice, there is still a major gap between the wide variety of non-classical logics that are investigated in the logic literature, and the few applications that use them. One possible explanation for this state of affairs is the lack of available tools for reasoning with non-classical logics, which requires the implementation of each logic from scratch.

In this talk I will present Gen2sat, a tool that makes it easier to implement a wide variety of propositional non-classical logics, including many paraconsistent logic and multi-valued logics. The key feature of Gen2sat is that its input consists not only of a logical formula, but also of a (proof theoretical) description of the logic in which the formula should be checked. This is done by a uniform reduction to SAT that goes through a general semantic interpretation of derivation rules. Shifting the intricacies of implementation and heuristic considerations to the realm of off-the-shelf SAT solvers, Gen2sat brings classical SAT-solver technology to the realm of non classical logics.

   Bio for Yoni Zohar

Yoni Zohar is a fifth-year PhD student at the school of computer science of Tel Aviv University. His research focuses on semantics and proof theory of non-classical logics.

   Note for Visitors to SRI

Please arrive at least 10 minutes early as you will need to sign in by following instructions by the lobby phone at Building E (or call Wilma Lenz at 650 859 4904, or Eunice Tseng at 650 859 2799). SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the parking lots off Fourth Street. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page. There are two entrances to SRI International located on Ravenswood Ave. Please check the Building E entrance signage.

SRI International
©2019 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy