@article{Baer2021,
  author    = {B{\"a}r, Christian},
  title     = {The Faddeev-LeVerrier algorithm and the Pfaffian},
  series = {Linear algebra and its applications},
  volume    = {630},
  journal   = {Linear algebra and its applications},
  publisher = {Elsevier},
  address   = {New York},
  issn      = {0024-3795},
  doi       = {10.1016/j.laa.2021.07.023},
  pages     = {39 -- 55},
  year      = {2021},
  abstract  = {We adapt the Faddeev-LeVerrier algorithm for the computation of characteristic polynomials to the computation of the Pfaffian of a skew-symmetric matrix. This yields a very simple, easy to implement and parallelize algorithm of computational cost O(n(beta+1)) where nis the size of the matrix and O(n(beta)) is the cost of multiplying n x n-matrices, beta is an element of [2, 2.37286). We compare its performance to that of other algorithms and show how it can be used to compute the Euler form of a Riemannian manifold using computer algebra.},
  language  = {en}
}
@article{Frank2012,
  author    = {Frank, Mario},
  title     = {Axiom relevance decision engine : technical report},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-72128},
  year      = {2012},
  abstract  = {This document presents an axiom selection technique for classic first order theorem proving based on the relevance of axioms for the proof of a conjecture. It is based on unifiability of predicates and does not need statistical information like symbol frequency. The scope of the technique is the reduction of the set of axioms and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the axiom set, it can be used as a preprocessor for automated theorem proving. This technical report describes the conception, implementation and evaluation of ARDE. The selection method, which is based on a breadth-first graph search by unifiability of predicates, is a weakened form of the connection calculus and uses specialised variants or unifiability to speed up the selection. The implementation of the concept is evaluated with comparison to the results of the world championship of theorem provers of the year 2012 (CASC J6). It is shown that both the theorem prover leanCoP which uses the connection calculus and E which uses equality reasoning, can benefit from the selection approach. Also, the evaluation shows that the concept is applyable for theorem proving problems with thousands of formulae and that the selection is independent from the calculus used by the theorem prover.},
  language  = {en}
}