6 citations · 7 across the 6 of their papers we have counts for
7 papers
Equal diffusions and zero Dirichlet boundary conditions can induce blow-up
Pavol Quittner, Philippe Souplet
For a class of systems of two parabolic equations with equal diffusion and homogeneous Dirichlet boundary conditions, we show the existence of finite time blow-up solutions, althou…
SATisfying the High School Identities but not Wilkie's Identity
Agon Hajdari, Johannes Niederhauser
We settle an open question related to Tarski's High School Algebra problem by showing that no 11-element algebra can satisfy the High School Identities while refuting Wilkie's iden…
Towards an HRS Category in TermCOMP
Johannes Niederhauser, Aart Middeldorp
We show that there is a simple syntactically-defined subclass of higher-order benchmarks in the termination problem database for which rewriting according to Nipkow's higher-order…
Unification of Deterministic Higher-Order Patterns (Full Version)
Johannes Niederhauser, Aart Middeldorp
We present a sound and complete unification procedure for deterministic higher-order patterns, a class of simply-typed lambda terms introduced by Yokoyama et al. which comes with a…
The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)
Johannes Niederhauser, Aart Middeldorp
We lift the computability path order and its extensions from plain higher-order rewriting to higher-order rewriting on beta-eta-normal forms where matching modulo beta-eta is emplo…
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving…
Left-Linear Completion with AC Axioms
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in…