OU Portal
  • Log In
  • Welcome
  • Applicants
Z6_60GI02O0O8IDC0QEJUJ26TJDI4
{}

Pomocí tohoto dialogu můžete vyhledat domácí autory, čili autory, kteří jsou vedeni v personálních systémech Ostravské univerzity.

Do našeptávače níže napište hledaný text a tento text bude vyhledán ve jméně nebo příjmení autora. Autoři, kteří budou hledanému textu odpovídat, Vám budou nabídnuti v seznamu. Pomocí myši nebo šipek na klávesnici vyberte požadovaného autora.

Našeptávač : 
Přidat autora k záznamu Zavřít

Pomocí tohoto dialogu můžete k záznamu přidat cizího autora, čili autora, který nemá žádný pracovní ani studijní vztah k Ostravské univerzitě. Takto přidaný autor bude do RIV vykázán jako nedomácí.

Pro přidání autora vepište jeho jméno a příjmení do určených položek.

Jméno :
Příjmení :
Přidat k záznamu Zavřít
Zavřít
Publikační činnost


preloading...   Probíhá načítání, čekejte prosím...
publicationId :
tempRecordId :
actionDispatchIndex :
navigationBranch :
pageMode :
tabSelected :
isRivValid :
Typ záznamu * : prezentace (kongresy, sympózia, konference, workshopy)
Domácí pracoviště * : Ústav pro výzkum a aplikace fuzzy modelování (94410)
Název * : Graph Neural Networks in Automated Reasoning
Citace : MOJŽÍŠEK, D. Graph Neural Networks in Automated Reasoning. In: ISCAMI 2020. Malenovice. 2020.
Podnázev :
Rok : 2020
Obor : Informatika
Místo konání : Malenovice
Stát konání akce : Česká republika
Název akce : ISCAMI 2020
Datum od :
Datum do :
Druh prezentace : Přednáška
Instituce :
Klíčová slova anglicky :
GNN, automated reasoning, neural networks
Popis v původním jazyce :
In this contribution, we will demonstrate how Graph Neural Networks (GNNs) can be utilized in the field of automated reasoning, specifically in theorem proving. Proving process can be viewed as a transition from one state to another. Logical formulae are transformed by applying specific and strictly given rules (or applying previously proven propositions). The goal is to find the chain of such formulae in which each formula is logically consequent to the previous one (by those rules). The last formula in that chain is the one to be proved. Such a chain is called a proof. We can see that graph-structure is inherent to the data connected to logical proofs. The whole process of proving may be seen as a walk through the graph whose nodes are particular expressions and edges are possible transitions. The agent performing the proof has to choose the correct sequence of steps. Logical formulae can also be parsed and encoded as a syntactic tree that is also a graph. Graph Neural Network is a strong tool that can be used to process various graph-structured data. For example, it can be used to encode nodes or whole graph by mapping them to real vectors. Those vectors offer other possibilities for processing (we can, for example, measure their similarity). We aim to explain how exactly GNNs can be incorporated in theorem proving, introduce existing frameworks and propose our future research in the area. Of course, the proving process as a whole is very complex and for that reason, it is convenient to find solutions to its sub-problems rather than whole proof. Those sub-problems include tasks like proof validation or premise selection. Our talk will be centered around those sub-problems.
Popis v anglickém jazyce :
Typ zdroje financování výsledku :
Seznam projektů :
ID Projektu Název projektu
Seznam ohlasů : 
Ohlas
R01:

© 2019 Centre for Information Technology

  • Technická podpora :
  • Mgr. Olga Blahutová (phone: +420 597 091 129, phone flap for UO: 1129)
  • Ing. Lucie Svitaneková (phone: +420 597 091 108, phone flap for UO: 1108)
Complementary Content
  • ${title}${badge}
${loading}