Search

Your search keyword '"Vukmirović, Petar"' showing total 26 results
Start Over Author "Vukmirović, Petar"

Refine your results

more »

more »

more »
26 results on '"Vukmirović, Petar"'

1. SAT-Inspired Higher-Order Eliminations

Author

Blanchette, Jasmin and Vukmirović, Petar

Subjects
Computer Science - Logic in Computer Science
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 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.

Published
2022
Full Text
View/download PDF

2. Superposition with Lambdas

Author

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

Subjects
Computer Science - Logic in Computer Science, Computer Science - Artificial Intelligence, F.4.1, I.2.3
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 $\beta\eta$-equivalence classes of $\lambda$-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.

Published
2021

3. Efficient Full Higher-Order Unification

Author

Vukmirović, Petar, Bentkamp, Alexander, and Nummelin, Visa

Subjects
Computer Science - Logic in Computer Science
Abstract

We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set of unifiers. We identify a new such fragment and describe a procedure for computing its unifiers. Our unification procedure, together with new higher-order term indexing data structures, is implemented in the Zipperposition theorem prover. Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski's procedure.

Published
2020
Full Text
View/download PDF

4. Extending a High-Performance Prover to Higher-Order Logic

Author

Vukmirović, Petar, Blanchette, Jasmin, Schulz, Stephan, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Sankaranarayanan, Sriram, editor, and Sharygina, Natasha, editor

Published
2023
Full Text
View/download PDF

8. Making Higher-Order Superposition Work

Author

Vukmirović, Petar, Bentkamp, Alexander, Blanchette, Jasmin, Cruanes, Simon, Nummelin, Visa, Tourret, Sophie, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Platzer, André, editor, and Sutcliffe, Geoff, editor

Published
2021
Full Text
View/download PDF

9. Superposition with First-class Booleans and Inprocessing Clausification

Author

Nummelin, Visa, Bentkamp, Alexander, Tourret, Sophie, Vukmirović, Petar, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Platzer, André, editor, and Sutcliffe, Geoff, editor

Published
2021
Full Text
View/download PDF

10. Superposition for Full Higher-order Logic

Author

Bentkamp, Alexander, Blanchette, Jasmin, Tourret, Sophie, Vukmirović, Petar, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Platzer, André, editor, and Sutcliffe, Geoff, editor

Published
2021
Full Text
View/download PDF

12. Superposition with Lambdas

Author

Bentkamp, Alexander, Blanchette, Jasmin, Tourret, Sophie, Vukmirović, Petar, Waldmann, Uwe, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Fontaine, Pascal, editor

Published
2019
Full Text
View/download PDF

13. Faster, Higher, Stronger: E 2.3

Author

Schulz, Stephan, Cruanes, Simon, Vukmirović, Petar, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Fontaine, Pascal, editor

Published
2019
Full Text
View/download PDF

14. Extending a Brainiac Prover to Lambda-Free Higher-Order Logic

Author

Vukmirović, Petar, Blanchette, Jasmin Christian, Cruanes, Simon, Schulz, Stephan, Hutchison, David, Editorial Board Member, Kanade, Takeo, Editorial Board Member, Kittler, Josef, Editorial Board Member, Kleinberg, Jon M., Editorial Board Member, Mattern, Friedemann, Editorial Board Member, Mitchell, John C., Editorial Board Member, Naor, Moni, Editorial Board Member, Pandu Rangan, C., Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Terzopoulos, Demetri, Editorial Board Member, Tygar, Doug, Editorial Board Member, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Vojnar, Tomáš, editor, and Zhang, Lijun, editor

Published
2019
Full Text
View/download PDF

17. Making Higher-Order Superposition Work

Author

Vukmirović, Petar, primary, Bentkamp, Alexander, additional, Blanchette, Jasmin, additional, Cruanes, Simon, additional, Nummelin, Visa, additional, and Tourret, Sophie, additional

Published
2021
Full Text
View/download PDF

18. Mechanical Mathematicians.

Author

BENTKAMP, ALEXANDER, BLANCHETTE, JASMIN, NUMMELIN, VISA, TOURRET, SOPHIE, VUKMIROVIĆ, PETAR, and WALDMANN, UWE

Subjects
MATHEMATICIANS, MATHEMATICAL proofs, COMPUTER systems, ALGEBRA, LOGICAL prediction
Abstract

The article discusses the challenges in designing an efficient computer-oriented approach to mathematical theorem proving for higher-order reasoning. Evaluations of several higher-order provers based on superposition and satisfiability modulo theories (SMT) are evaluated.

Published
2023
Full Text
View/download PDF

22. Seventeen Provers Under the Hammer

Author

Martin Desharnais and Petar Vukmirović and Jasmin Blanchette and Makarius Wenzel, Desharnais, Martin, Vukmirović, Petar, Blanchette, Jasmin, Wenzel, Makarius, Martin Desharnais and Petar Vukmirović and Jasmin Blanchette and Makarius Wenzel, Desharnais, Martin, Vukmirović, Petar, Blanchette, Jasmin, and Wenzel, Makarius

Abstract

One of the main success stories of automatic theorem provers has been their integration into proof assistants. Such integrations, or "hammers," increase proof automation and hence user productivity. In this paper, we use Isabelle/HOL’s Sledgehammer tool to find out how useful modern provers are at proving formulas in higher-order logic. Our evaluation follows in the steps of Böhme and Nipkow’s Judgment Day study from 2010, but instead of three provers we use 17, including SMT solvers and higher-order provers. Our work offers an alternative yardstick for comparing modern provers, next to the benchmarks and competitions emerging from the TPTP World and SMT-LIB.

Published
2022
Full Text
View/download PDF

24. Superposition with Lambdas

Author

Bentkamp, Alexander, primary, Blanchette, Jasmin, additional, Tourret, Sophie, additional, Vukmirović, Petar, additional, and Waldmann, Uwe, additional

Published
2021
Full Text
View/download PDF

26. Efficient Full Higher-Order Unification

Author

Petar Vukmirović and Alexander Bentkamp and Visa Nummelin, Vukmirović, Petar, Bentkamp, Alexander, Nummelin, Visa, Petar Vukmirović and Alexander Bentkamp and Visa Nummelin, Vukmirović, Petar, Bentkamp, Alexander, and Nummelin, Visa

Abstract

We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set of unifiers. We identify a new such fragment and describe a procedure for computing its unifiers. Our unification procedure is implemented in the Zipperposition theorem prover. Experimental evaluation shows a clear advantage over Jensen and Pietrzykowski’s procedure.

Published
2020
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results