Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

13 résultats
Image document

Proving Determinacy of the PharOS Real-Time Operating System

Selma Azaiez , Damien Doligez , Matthieu Lemerre , Tomer Libal , Stephan Merz
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩
Communication dans un congrès hal-01322335v1
Image document

A general proof certification framework for modal logic

Tomer Libal , Marco Volpe
[Research Report] INRIA. 2017
Rapport hal-01643126v1
Image document

Defining the meaning of TPTP formatted proofs

Roberto Blanco , Tomer Libal , Dale Miller
11th International Workshop on the Implementation of Logics, Nov 2015, Suva, Fiji
Communication dans un congrès hal-01238434v1

Regular Patterns in Second-Order Unification

Tomer Libal
Proceedings of CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, Aug 2015, Berlin, Germany. ⟨10.1007/978-3-319-21401-6_38⟩
Communication dans un congrès hal-01242215v1
Image document

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

Damien Doligez , Jael Kriener , Leslie Lamport , Tomer Libal , Stephan Merz
ARQNL 2014 - The first International Workshop on Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. pp.1-16
Communication dans un congrès hal-01063512v1

Functions-as-constructors higher-order unification: extended pattern unification

Tomer Libal , Dale Miller
Annals of Mathematics and Artificial Intelligence, 2021, ⟨10.1007/s10472-021-09774-y⟩
Article dans une revue hal-03457303v1
Image document

Functions-as-constructors Higher-order Unification

Tomer Libal , Dale Miller
1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Delia Kesner and Brigitte Pientka, Jun 2016, Porto, Portugal. pp.1 - 17, ⟨10.4230/LIPIcs.FSCD.2016.26⟩
Communication dans un congrès hal-01379683v1
Image document

Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers

Tomer Libal , Alexander Steen
5th Workshop on Practical Aspects of Automated Reasoning, Jul 2016, Coimbra, Portugal
Communication dans un congrès hal-01424749v1

A validation process for a legal formalization method

Abdelhamid Abidi , Tomer Libal
LN2FR – METHODOLOGIES FOR TRANSLATING LEGAL NORMS INTO FORMAL REPRESENTATIONS, Université de Sarrebruck, Dec 2022, Saarbrücken, France
Communication dans un congrès hal-03941560v1
Image document

System Description: The Proof Transformation System CERES

Tsvetan Dunchev , Alexander Leitsch , Tomer Libal , Daniel Weller , Bruno Woltzenlogel Paleo
International Joint Conference on Automated Reasoning, Jul 2010, Edinburgh, United Kingdom. pp.427-433, ⟨10.1007/978-3-642-14203-1_36⟩
Communication dans un congrès hal-00545482v1
Image document

Certification of labeled proofs for modal logics with geometric frame conditions

Tomer Libal , Marco Volpe
2017
Pré-publication, Document de travail hal-01643120v1
Image document

The Proof Certifier Checkers

Zakaria Chihani , Tomer Libal , Giselle Reis
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Sep 2015, Wroclaw, Poland. pp.201-210, ⟨10.1007/978-3-319-24312-2_14⟩
Communication dans un congrès hal-01208333v1
Image document

The Dawn of the Human-Machine Era: A forecast of new and emerging language technologies.

Dave Sayers , Rui Sousa-Silva , Sviatlana Höhn , Lule Ahmedi , Kais Allkivi-Metsoja , et al.
2021
Autre publication scientifique hal-03230287v1