2 Search Results for "Tinelli, Cesare"

Document

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)

Authors: Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli

Published in: Dagstuhl Reports, Volume 9, Issue 9 (2020)

Abstract

Research in automated deduction is traditionally focused on the problem of determining the satisfiability of formulas or, more generally, on solving logical problems with yes/no answers. Thanks to recent advances that have dramatically increased the power of automated deduction tools, there is now a growing interest in extending deduction techniques to attack logical problems with more complex answers. These include both problems with a long history, such as quantifier elimination, which are now being revisited in light of the new methods, as well as newer problems such as minimal unsatisfiable cores computation, model counting for propositional or first-order formulas, Boolean or SMT constraint optimization, generation of interpolants, abductive reasoning, and syntax-guided synthesis. Such problems arise in a variety of applications including the analysis of probabilistic systems (where properties like safety or liveness can be established only probabilistically), network verification (with relies on model counting), the computation of tight complexity bounds for programs, program synthesis, model checking (where interpolation or abductive reasoning can be used to achieve scale), and ontology-based information processing. The seminar brought together researchers and practitioners from many of the often disjoint sub-communities interested in the problems above. The unifying theme of the seminar was how to harness and extend the power of automated deduction methods to solve problems with more complex answers than binary ones.

Cite as

Carsten Fuhs, Philipp Rümmer, Renate Schmidt, and Cesare Tinelli. Deduction Beyond Satisfiability (Dagstuhl Seminar 19371). In Dagstuhl Reports, Volume 9, Issue 9, pp. 23-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{fuhs_et_al:DagRep.9.9.23,
  author =	{Fuhs, Carsten and R\"{u}mmer, Philipp and Schmidt, Renate and Tinelli, Cesare},
  title =	{{Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)}},
  pages =	{23--44},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2020},
  volume =	{9},
  number =	{9},
  editor =	{Fuhs, Carsten and R\"{u}mmer, Philipp and Schmidt, Renate and Tinelli, Cesare},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.9.9.23},
  URN =		{urn:nbn:de:0030-drops-118432},
  doi =		{10.4230/DagRep.9.9.23},
  annote =	{Keywords: abduction, automated deduction, interpolation, quantifier elimination, synthesis}
}

Document

DOI: 10.4230/DagRep.7.9.26

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

Authors: Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 17371 "Deduction Beyond First-Order Logic." Much research in the past two decades was dedicated to automating first-order logic with equality. However, applications often need reasoning beyond this logic. This includes genuinely higher-order reasoning, reasoning in theories that are not finitely axiomatisable in first-order logic (such as those including transitive closure operators or standard arithmetic on integers or reals), or reasoning by mathematical induction. Other practical problems need a mixture of first-order proof search and some more advanced reasoning (for instance, about higher-order formulas), or simply higher-level reasoning steps. The aim of the seminar was to bring together first-order automated reasoning experts and researchers working on deduction methods and tools that go beyond first-order logic. The seminar was dedicated to the exchange of ideas to facilitate the transition from first-order to more expressive settings.

Cite as

Jasmin Christian Blanchette, Carsten Fuhs, Viorica Sofronie-Stokkermans, and Cesare Tinelli. Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). In Dagstuhl Reports, Volume 7, Issue 9, pp. 26-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{blanchette_et_al:DagRep.7.9.26,
  author =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
  title =	{{Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)}},
  pages =	{26--46},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Blanchette, Jasmin Christian and Fuhs, Carsten and Sofronie-Stokkermans, Viorica and Tinelli, Cesare},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.9.26},
  URN =		{urn:nbn:de:0030-drops-85872},
  doi =		{10.4230/DagRep.7.9.26},
  annote =	{Keywords: Automated Deduction, Program Verification, Certification}
}

Refine by Author
2 Fuhs, Carsten
2 Tinelli, Cesare
1 Blanchette, Jasmin Christian
1 Rümmer, Philipp
1 Schmidt, Renate
Show More...

Refine by Classification

Refine by Keyword
1 Automated Deduction
1 Certification
1 Program Verification
1 abduction
1 automated deduction
Show More...

Refine by Type
2 document

Refine by Publication Year
1 2018
1 2020

2 Search Results for "Tinelli, Cesare"

Deduction Beyond Satisfiability (Dagstuhl Seminar 19371)

Abstract

Cite as

Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)

Abstract

Cite as

Thanks for your feedback!

Could not send message