Open AccessAn Inference Rule for the Acyclicity Property of Term Algebras
Author(s) -
Simon Robillard
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/tlw4
Subject(s) - automated theorem proving , term (time) , axiom , gas meter prover , mathematical proof , property (philosophy) , computer science , rule of inference , inference , natural deduction , calculus (dental) , mathematics , theoretical computer science , algebra over a field , algorithm , discrete mathematics , programming language , artificial intelligence , pure mathematics , quantum mechanics , medicine , philosophy , physics , geometry , dentistry , epistemology
Term algebras are important structures in many areas of mathematics and computer science. Reasoning about their theories in superposition-based first-order theorem provers is made difficult by the acyclicity property of terms, which is not finitely axiomatizable. We present an inference rule that extends the superposition calculus and allows reasoning about term algebras without axioms to describe the acyclicity property. We detail an indexing technique to efficiently apply this rule in problems containing a large number of clauses. Finally we experimentally evaluate an implementation of this extended calculus in the first-order theorem prover Vampire. The results show that this technique is able to find proofs for difficult problems that existing SMT solvers and first-order theorem provers are unable to solve.