5 Search Results for "Gupta, Gopal"


Document
Coinduction in Flow: The Later Modality in Fibrations

Authors: Henning Basold

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)


Abstract
This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The construction is essentially a generalisation of the topos of trees from the codomain fibration over sets to arbitrary fibrations. As a result, we obtain a framework that allows the addition of a recursion principle for coinduction to rather arbitrary logics and programming languages. The main interest of using recursion is that it allows one to write proofs and programs in a goal-oriented fashion. This enables easily understandable coinductive proofs and programs, and fosters automatic proof search. Part of the framework are also various results that enable a wide range of applications: transportation of (co)limits, exponentials, fibred adjunctions and first-order connectives from the initial fibration to the one constructed through the framework. This means that the framework extends any first-order logic with the later modality. Moreover, we obtain soundness and completeness results, and can use up-to techniques as proof rules. Since the construction works for a wide variety of fibrations, we will be able to use the recursion offered by the later modality in various context. For instance, we will show how recursive proofs can be obtained for arbitrary (syntactic) first-order logics, for coinductive set-predicates, and for the probabilistic modal mu-calculus. Finally, we use the same construction to obtain a novel language for probabilistic productive coinductive programming. These examples demonstrate the flexibility of the framework and its accompanying results.

Cite as

Henning Basold. Coinduction in Flow: The Later Modality in Fibrations. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{basold:LIPIcs.CALCO.2019.8,
  author =	{Basold, Henning},
  title =	{{Coinduction in Flow: The Later Modality in Fibrations}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{8:1--8:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.8},
  URN =		{urn:nbn:de:0030-drops-114369},
  doi =		{10.4230/LIPIcs.CALCO.2019.8},
  annote =	{Keywords: Coinduction, Fibrations, Later Modality, Recursive Proofs, Up-to techniques, Probabilistic Logic, Probabilistic Programming}
}
Document
A Coalgebraic Perspective on Probabilistic Logic Programming

Authors: Tao Gu and Fabio Zanasi

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)


Abstract
Probabilistic logic programming is increasingly important in artificial intelligence and related fields as a formalism to reason about uncertainty. It generalises logic programming with the possibility of annotating clauses with probabilities. This paper proposes a coalgebraic perspective on probabilistic logic programming. Programs are modelled as coalgebras for a certain functor F, and two semantics are given in terms of cofree coalgebras. First, the cofree F-coalgebra yields a semantics in terms of derivation trees. Second, by embedding F into another type G, as cofree G-coalgebra we obtain a "possible worlds" interpretation of programs, from which one may recover the usual distribution semantics of probabilistic logic programming.

Cite as

Tao Gu and Fabio Zanasi. A Coalgebraic Perspective on Probabilistic Logic Programming. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gu_et_al:LIPIcs.CALCO.2019.10,
  author =	{Gu, Tao and Zanasi, Fabio},
  title =	{{A Coalgebraic Perspective on Probabilistic Logic Programming}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{10:1--10:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.10},
  URN =		{urn:nbn:de:0030-drops-114387},
  doi =		{10.4230/LIPIcs.CALCO.2019.10},
  annote =	{Keywords: probabilistic logic programming, coalgebraic semantics, distribution semantics}
}
Document
Formalizing the Solution to the Cap Set Problem

Authors: Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of F^n_q with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case q = 3, where it is commonly known as the cap set problem. Ellenberg and Gijswijt’s proof was published in the Annals of Mathematics and is noteworthy for its clever use of elementary methods. This paper describes a formalization of this proof in the Lean proof assistant, including both the general result in F^n_q and concrete values for the case q = 3. We faithfully follow the pen and paper argument to construct the bound. Our work shows that (some) modern mathematics is within the range of proof assistants.

Cite as

Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{dahmen_et_al:LIPIcs.ITP.2019.15,
  author =	{Dahmen, Sander R. and H\"{o}lzl, Johannes and Lewis, Robert Y.},
  title =	{{Formalizing the Solution to the Cap Set Problem}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{15:1--15:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.15},
  URN =		{urn:nbn:de:0030-drops-110703},
  doi =		{10.4230/LIPIcs.ITP.2019.15},
  annote =	{Keywords: formal proof, combinatorics, cap set problem, Lean}
}
Document
Cumulative Scoring-Based Induction of Default Theories

Authors: Farhad Shakerin and Gopal Gupta

Published in: OASIcs, Volume 64, Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)


Abstract
Significant research has been conducted in recent years to extend Inductive Logic Programming (ILP) methods to induce a more expressive class of logic programs such as answer set programs. The methods proposed perform an exhaustive search for the correct hypothesis. Thus, they are sound but not scalable to real-life datasets. Lack of scalability and inability to deal with noisy data in real-life datasets restricts their applicability. In contrast, top-down ILP algorithms such as FOIL, can easily guide the search using heuristics and tolerate noise. They also scale up very well, due to the greedy nature of search for best hypothesis. However, in some cases despite having ample positive and negative examples, heuristics fail to direct the search in the correct direction. In this paper, we introduce the FOLD 2.0 algorithm - an enhanced version of our recently developed algorithm called FOLD. Our original FOLD algorithm automates the inductive learning of default theories. The enhancements presented here preserve the greedy nature of hypothesis search during clause specialization. These enhancements also avoid being stuck in local optima - a major pitfall of FOIL-like algorithms. Experiments that we report in this paper, suggest a significant improvement in terms of accuracy and expressiveness of the class of induced hypotheses. To the best of our knowledge, our FOLD 2.0 algorithm is the first heuristic based, scalable, and noise-resilient ILP system to induce answer set programs.

Cite as

Farhad Shakerin and Gopal Gupta. Cumulative Scoring-Based Induction of Default Theories. In Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). Open Access Series in Informatics (OASIcs), Volume 64, pp. 2:1-2:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{shakerin_et_al:OASIcs.ICLP.2018.2,
  author =	{Shakerin, Farhad and Gupta, Gopal},
  title =	{{Cumulative Scoring-Based Induction of Default Theories}},
  booktitle =	{Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)},
  pages =	{2:1--2:15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-090-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{64},
  editor =	{Dal Palu', Alessandro and Tarau, Paul and Saeedloei, Neda and Fodor, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2018.2},
  URN =		{urn:nbn:de:0030-drops-98685},
  doi =		{10.4230/OASIcs.ICLP.2018.2},
  annote =	{Keywords: Inductive Logic Programming, Negation As Failure, Answer Set Programming, Default reasoning, Machine learning}
}
Document
Timed Definite Clause Omega-Grammars

Authors: Neda Saeedloei and Gopal Gupta

Published in: LIPIcs, Volume 7, Technical Communications of the 26th International Conference on Logic Programming (2010)


Abstract
We propose timed context-free grammars (TCFGs) and show how parsers for such grammars can be developed using definite clause grammars (DCGs) coupled with constraints over reals (CLP(R)). Timed context-free grammars describe timed context-free languages (TCFLs). We next extend timed context-free grammars to timed context-free omega-grammars (omega-TCFGs for brevity) and incorporate co-inductive logic programming in DCGs to obtain parsers for them. Timed context-free omega-grammars describe timed context-free languages containing infinite-sized words, and are a generalization of timed omega-regular languages recognized by timed automata. We show a practical application of omega-TCFGs to the well-known generalized railroad crossing problem.

Cite as

Neda Saeedloei and Gopal Gupta. Timed Definite Clause Omega-Grammars. In Technical Communications of the 26th International Conference on Logic Programming. Leibniz International Proceedings in Informatics (LIPIcs), Volume 7, pp. 212-221, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{saeedloei_et_al:LIPIcs.ICLP.2010.212,
  author =	{Saeedloei, Neda and Gupta, Gopal},
  title =	{{Timed Definite Clause Omega-Grammars}},
  booktitle =	{Technical Communications of the 26th International Conference on Logic Programming},
  pages =	{212--221},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-17-0},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{7},
  editor =	{Hermenegildo, Manuel and Schaub, Torsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2010.212},
  URN =		{urn:nbn:de:0030-drops-25994},
  doi =		{10.4230/LIPIcs.ICLP.2010.212},
  annote =	{Keywords: Constraint Logic Programming over reals, Co-induction, Context-Free Grammars, Omega-Grammars}
}
  • Refine by Author
  • 2 Gupta, Gopal
  • 1 Basold, Henning
  • 1 Dahmen, Sander R.
  • 1 Gu, Tao
  • 1 Hölzl, Johannes
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Logic
  • 1 Computing methodologies → Combinatorial algorithms
  • 1 Computing methodologies → Inductive logic learning
  • 1 Mathematics of computing → Number-theoretic computations
  • 1 Software and its engineering → Formal methods
  • Show More...

  • Refine by Keyword
  • 1 Answer Set Programming
  • 1 Co-induction
  • 1 Coinduction
  • 1 Constraint Logic Programming over reals
  • 1 Context-Free Grammars
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 3 2019
  • 1 2010
  • 1 2018

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail