Research

  2021

Functions-as-constructors Higher-order Unification, Extended Pattern Unification

Tomer Libal, Dale Miller [ ORIGINAL ]

  2021

Towards Transparent Legal Formalization

Tomer Libal, Tereza Novotna [ DRAFT ]

  2020

A bimodal simulation of defeasibility in the normative domain

Tomer Libal, Matteo Pascucci, Leendert van der Torre and Dov Gabbay [ DRAFT ]

  2020

Towards Automated GDPR Compliance Checking

Tomer Libal [ DRAFT ]

  2020

A Meta-level Annotation Language for Legal Texts

Tomer Libal [ DRAFT ]

  2020

Towards an Executable Methodology for the Formalization of Legal Texts

Tomer Libal and Alexander Steen [ DRAFT ]

  2020

Towards Automating Inconsistency Checking of Legal Texts

Tomer Libal, Tereza Novotná [ DRAFT ]

  2020

NAI - Towards Transparent and Usable Semi-Automated Legal Analysis

Tomer Libal, Alexander Steen [ DRAFT ]

  2019

The NAI Suite – Drafting and Reasoning over Legal Texts

Tomer Libal, Alexander Steen [ DRAFT ]

  2019

Automated Reasoning in Normative Detachment Structures with Ideal Conditions

Tomer Libal, Matteo Pascucci [ DRAFT ]

  2019

NAI – The Normative Reasoner

Tomer Libal, Alexander Steen [ DRAFT ]

  2019

A general proof certification framework for modal logic

Tomer Libal, Marco Volpe [ DRAFT ]

  2018

A Simple Semi-automated Proof Assistant for First-order Modal Logics

Tomer Libal [ DRAFT ]

  2018

Implementing a Proof Assistant using Focusing and Logic Programming

Tomer Libal [ DRAFT ]

  2017

Determinism in the Certification of UNSAT Proofs

Tomer Libal, Xaviera Steele [ DRAFT ]

  2017

Certification of labeled proofs for modal logics with geometric frame conditions (Research Report)

Tomer Libal, Marco Volpe [ DRAFT ]

  2017

A general proof certification framework for modal logic (Research Report)

Tomer Libal, Marco Volpe [ DRAFT ]

  2016

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

Tomer Libal, Alexander Steen [ DRAFT ]

  2016

Certification of Prefixed Tableau Proofs for Modal Logic

Tomer Libal, Marco Volpe [ DRAFT ]

  2016

Functions-as-Constructors Higher-Order Unification

Tomer Libal, Dale Miller [ DRAFT ]

  2016

Proving Determinacy of the PharOS Real-Time Operating System

Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz [ DRAFT ]

  2015

The Proof Certifier Checkers

Zakaria Chihani, Tomer Libal, Giselle Reis [ DRAFT ]

  2015

Defining the meaning of TPTP formatted proofs

Roberto Blanco, Tomer Libal, and Dale Miller [ DRAFT ]

  2015

Regular Patterns in Second-Order Unification

Tomer Libal [ DRAFT ]

  2014

Advanced Proof Viewing in ProofTool

Tomer Libal, Martin Riener, Mikheil Rukhaia [ DRAFT ]

  2014

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

Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz [ DRAFT ]

  2013

PROOFTOOL: a GUI for the GAPT Framework

Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel Paleo [ DRAFT ]

  2013

Understanding Resolution Proofs through Herbrand's Theorem

Stefan Hetzl, Tomer Libal, Martin Riener, Mikheil Rukhaia [ DRAFT ]

  2013

Utilizing Higher-order Unifiability Algorithms in the Resolution Calculus

Tomer Libal [ DRAFT ]

  2012

Bounded Higher-order Unification using Regular Terms

Tomer Libal [ DRAFT ]

  2012

System Feature Description: Importing Refutations into the GAPT Framework

Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel-Paleo [ DRAFT ]

  2012

A Resolution Calculus for Second-order Logic with Eager Unification

Alexander Leitsch, Tomer Libal [ DRAFT ]

  2010

System Description: The Proof Transformation System CERES

Tsvetan Dunchev, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo [ DRAFT ]

  2009

Resolution Refinements for Cut-Elimination based on Reductive Methods

Stefan Hetzl, Alexander Leitsch, Tomer Libal, Daniel Weller, Bruno Woltzenlogel Paleo [ DRAFT ]