Certifying Proofs in the First-Order Theory of Rewriting.

Fabian Mitterwallner Alexander Lochmann Aart Middeldorp Bertram Felgenhauer

Published in: TACAS (2) (2021)

Keyphrases

quantifier elimination
presburger arithmetic
theoretical basis
higher order
theoretical framework
theorem prover
quantifier free
databases
conjunctive queries
theorem proving
general theory
computational model
term rewriting