Search

Your search keyword '"Andreas Teucke"' showing total 8 results
Start Over Author "Andreas Teucke"
8 results on '"Andreas Teucke"'

7. SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment

Author

Christoph Weidenbach, Andreas Teucke, Max Planck Institute for Informatics [Saarbrücken], Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft

Subjects
Selection (relational algebra), First-Order Theorem Proving, Model Generation, 0102 computer and information sciences, 02 engineering and technology, Decidability, 01 natural sciences, Prime (order theory), Set (abstract data type), Fragment (logic), Artificial Intelligence, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Mathematics, Discrete mathematics, 020207 software engineering, Resolution (logic), Approximation Refinement, Automated theorem proving, Transformation (function), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, Software
Abstract

We introduce FO-AR, an approximation-refinement approach for first-order theorem proving based on counterexample-guided abstraction refinement. A given first-order clause set N is transformed into an over-approximation $$N^{\prime }$$ in a decidable first-order fragment. That means if $$N^{\prime }$$ is satisfiable so is N. However, if $$N^{\prime }$$ is unsatisfiable, then the approximation provides a lifting terminology for the found refutation which is step-wise transformed into a proof of unsatisfiability for N. If this fails, the cause is analyzed to refine the original clause set such that the found refutation is ruled out for the future and the procedure repeats. The target fragment of the transformation is the monadic shallow linear fragment with straight dismatching constraints, which we prove to be decidable via ordered resolution with selection. We further discuss practical aspects of SPASS-AR, a first-order theorem prover implementing FO-AR. We focus in particularly on effective algorithms for lifting and refinement.

Published
2020
Full Text
View/download PDF

8. Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints

Author

Christoph Weidenbach, Andreas Teucke, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, de Moura, Leonardo, Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, Discrete mathematics, Computer Science - Logic in Computer Science, Logic in computer science, Open problem, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Monadic predicate calculus, Logic in Computer Science (cs.LO), Decidability, Automaton, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Fragment (logic), 010201 computation theory & mathematics, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Tree (set theory), Computer Science::Formal Languages and Automata Theory, Mathematics, Resolution (algebra)
Abstract

The monadic shallow linear Horn fragment is well-known to be decidable and has many application, e.g., in security protocol analysis, tree automata, or abstraction refinement. It was a long standing open problem how to extend the fragment to the non-Horn case, preserving decidability, that would, e.g., enable to express non-determinism in protocols. We prove decidability of the non-Horn monadic shallow linear fragment via ordered resolution further extended with dismatching constraints and discuss some applications of the new decidable fragment., Comment: 29 pages, long version of CADE-26 paper

Published
2017
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results