Showing 1–10 of 10 results for author: Blanchette, J

Closure Properties of General Grammars -- Formally Verified

Authors: Martin Dvorak, Jasmin Blanchette

Abstract: We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to form… ▽ More We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four operations: union, reversal, concatenation, and the Kleene star. The literature mostly focuses on Turing machine arguments, which are possibly more difficult to formalize. For the Kleene star, we could not follow the literature and came up with our own grammar-based construction. △ Less

Submitted 22 May, 2023; v1 submitted 13 February, 2023; originally announced February 2023.

Comments: Accepted for publication at ITP 2023; code: https://github.com/madvorak/grammars/tree/publish

SAT-Inspired Higher-Order Eliminations

Authors: Jasmin Blanchette, Petar Vukmirović

Abstract: We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure litera… ▽ More We generalize several propositional preprocessing techniques to higher-order logic, building on existing first-order generalizations. These techniques eliminate literals, clauses, or predicate symbols from the problem, with the aim of making it more amenable to automatic proof search. We also introduce a new technique, which we call quasipure literal elimination, that strictly subsumes pure literal elimination. The new techniques are implemented in the Zipperposition theorem prover. Our evaluation shows that they sometimes help prove problems originating from Isabelle formalizations and the TPTP library. △ Less

Submitted 5 May, 2023; v1 submitted 16 August, 2022; originally announced August 2022.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 2 (May 8, 2023) lmcs:9928

Superposition with Lambdas

Authors: Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović, Uwe Waldmann

Abstract: We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $βη$-equivalence classes of $λ$-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle b… ▽ More We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $βη$-equivalence classes of $λ$-terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning. △ Less

Submitted 31 January, 2021; originally announced February 2021.

ACM Class: F.4.1; I.2.3

Superposition for Lambda-Free Higher-Order Logic

Authors: Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Uwe Waldmann

Abstract: We introduce refutationally complete superposition calculi for intentional and extensional clausal $λ$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $λ$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calcu… ▽ More We introduce refutationally complete superposition calculi for intentional and extensional clausal $λ$-free higher-order logic, two formalisms that allow partial application and applied variables. The calculi are parameterized by a term order that need not be fully monotonic, making it possible to employ the $λ$-free higher-order lexicographic path and Knuth-Bendix orders. We implemented the calculi in the Zipperposition prover and evaluated them on Isabelle/HOL and TPTP benchmarks. They appear promising as a step** stone towards complete, highly efficient automatic theorem provers for full higher-order logic. △ Less

Submitted 9 April, 2021; v1 submitted 5 May, 2020; originally announced May 2020.

Comments: arXiv admin note: text overlap with arXiv:2102.00453

ACM Class: F.4.1; I.2.3

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 2 (April 12, 2021) lmcs:6455

A Curious Link Between Prime Numbers, the Maundy Cake Problem and Parallel Sorting

Authors: Jonathan Blanchette, Robert Laganière

Abstract: We present new theoretical algorithms that sums the n-ary comparators output in order to get the permutation indices in order to sort a sequence. By analysing the parallel ranking algorithm, we found that the special comparators number of elements it processes divide the number of elements to be sorted. Using the divide and conquer method, we can express the sorting problem into summing output of… ▽ More We present new theoretical algorithms that sums the n-ary comparators output in order to get the permutation indices in order to sort a sequence. By analysing the parallel ranking algorithm, we found that the special comparators number of elements it processes divide the number of elements to be sorted. Using the divide and conquer method, we can express the sorting problem into summing output of comparators taking a prime number of elements, given that this prime number divides the initial disordered sequence length. The number of sums is directly related to the Maundy cake problem. Furthermore, we provide a new sequence that counts the number of comparators used in the algorithms. △ Less

Submitted 4 November, 2019; v1 submitted 25 October, 2019; originally announced October 2019.

Comments: 10 pages, 2 figures, 3 tables, final version

Language and Proofs for Higher-Order SMT (Work in Progress)

Authors: Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine

Abstract: Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started in March 2017, is to extend the reasoning capabilities of SMT solvers and other autom… ▽ More Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started in March 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We also discuss how to augment the proof format of the SMT solver veriT to accommodate these new constructs and the solving techniques they require. △ Less

Submitted 5 December, 2017; originally announced December 2017.

Comments: In Proceedings PxTP 2017, arXiv:1712.00898

Journal ref: EPTCS 262, 2017, pp. 15-22

Encoding Monomorphic and Polymorphic Types

Authors: Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone

Abstract: Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining… ▽ More Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes. △ Less

Submitted 30 December, 2016; v1 submitted 28 September, 2016; originally announced September 2016.

Comments: LMCS-2014-1018

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 4 (April 27, 2017) lmcs:2628

Extending Nunchaku to Dependent Type Theory

Authors: Simon Cruanes, Jasmin Christian Blanchette

Abstract: Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes… ▽ More Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful. △ Less

Submitted 19 June, 2016; originally announced June 2016.

Comments: In Proceedings HaTT 2016, arXiv:1606.05427

Journal ref: EPTCS 210, 2016, pp. 3-12

Proceedings First International Workshop on Hammers for Type Theories

Authors: Jasmin Christian Blanchette, Cezary Kaliszyk

Abstract: This volume of EPTCS contains the proceedings of the First Workshop on Hammers for Type Theories (HaTT 2016), held on 1 July 2016 as part of the International Joint Conference on Automated Reasoning (IJCAR 2016) in Coimbra, Portugal. The proceedings contain four regular papers, as well as abstracts of the two invited talks by Pierre Corbineau (Verimag, France) and Aleksy Schubert (University of Wa… ▽ More This volume of EPTCS contains the proceedings of the First Workshop on Hammers for Type Theories (HaTT 2016), held on 1 July 2016 as part of the International Joint Conference on Automated Reasoning (IJCAR 2016) in Coimbra, Portugal. The proceedings contain four regular papers, as well as abstracts of the two invited talks by Pierre Corbineau (Verimag, France) and Aleksy Schubert (University of Warsaw, Poland). △ Less

Submitted 17 June, 2016; originally announced June 2016.

Journal ref: EPTCS 210, 2016

Foundational Extensible Corecursion

Authors: Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Abstract: This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing th… ▽ More This paper presents a formalized framework for defining corecursive functions safely in a total setting, based on corecursion up-to and relational parametricity. The end product is a general corecursor that allows corecursive (and even recursive) calls under well-behaved operations, including constructors. Corecursive functions that are well behaved can be registered as such, thereby increasing the corecursor's expressiveness. The metatheory is formalized in the Isabelle proof assistant and forms the core of a prototype tool. The corecursor is derived from first principles, without requiring new axioms or extensions of the logic. △ Less

Submitted 22 January, 2015; originally announced January 2015.

ACM Class: F.3.1; F.4.1