Research Reports
2016
Althaus, E., Beber, B., Damm, W., Disch, S., Hagemann, W., Rakow, A., … Wirtz, B. (2016). Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization (No. ATR103). SFB/TR 14 AVACS.
Abstract
This paper provides a suite of optimization techniques for
the verification of safety properties of linear hybrid
automata with large discrete state spaces, such as
naturally arising when incorporating health state
monitoring and degradation levels into the controller
design. Such models can -- in contrast to purely functional
controller models -- not analyzed with hybrid verification
engines relying on explicit representations of modes, but
require fully symbolic representations for both the
continuous and discrete part of the state space. The
optimization techniques shown yield consistently a speedup
of about 20 against previously published results for a
similar benchmark suite, and complement these with new
results on counterexample guided abstraction refinement. In
combination with the methods guaranteeing preciseness of
abstractions, this allows to significantly extend the class
of models for which safety can be established, covering in
particular models with 23 continuous variables and 2 to the
71 discrete states, 20 continuous variables and 2 to the
199 discrete states, and 9 continuous variables and 2 to
the 271 discrete states.
Export
BibTeX
@techreport{AlthausBeberDammEtAl2016ATR,
TITLE = {Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization},
AUTHOR = {Althaus, Ernst and Beber, Bj{\"o}rn and Damm, Werner and Disch, Stefan and Hagemann, Willem and Rakow, Astrid and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR103},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2016},
DATE = {2016},
ABSTRACT = {This paper provides a suite of optimization techniques for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can -- in contrast to purely functional controller models -- not analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The optimization techniques shown yield consistently a speedup of about 20 against previously published results for a similar benchmark suite, and complement these with new results on counterexample guided abstraction refinement. In combination with the methods guaranteeing preciseness of abstractions, this allows to significantly extend the class of models for which safety can be established, covering in particular models with 23 continuous variables and 2 to the 71 discrete states, 20 continuous variables and 2 to the 199 discrete states, and 9 continuous variables and 2 to the 271 discrete states.},
TYPE = {AVACS Technical Report},
VOLUME = {103},
}
Endnote
%0 Report
%A Althaus, Ernst
%A Beber, Björn
%A Damm, Werner
%A Disch, Stefan
%A Hagemann, Willem
%A Rakow, Astrid
%A Scholl, Christoph
%A Waldmann, Uwe
%A Wirtz, Boris
%+ Algorithms and Complexity, MPI for Informatics, Max Planck Society
Algorithms and Complexity, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
International Max Planck Research School, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Verification of Linear Hybrid Systems with Large Discrete
State Spaces: Exploring the Design Space for Optimization :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002C-4540-0
%Y SFB/TR 14 AVACS
%D 2016
%P 93 p.
%X This paper provides a suite of optimization techniques for
the verification of safety properties of linear hybrid
automata with large discrete state spaces, such as
naturally arising when incorporating health state
monitoring and degradation levels into the controller
design. Such models can -- in contrast to purely functional
controller models -- not analyzed with hybrid verification
engines relying on explicit representations of modes, but
require fully symbolic representations for both the
continuous and discrete part of the state space. The
optimization techniques shown yield consistently a speedup
of about 20 against previously published results for a
similar benchmark suite, and complement these with new
results on counterexample guided abstraction refinement. In
combination with the methods guaranteeing preciseness of
abstractions, this allows to significantly extend the class
of models for which safety can be established, covering in
particular models with 23 continuous variables and 2 to the
71 discrete states, 20 continuous variables and 2 to the
199 discrete states, and 9 continuous variables and 2 to
the 271 discrete states.
%B AVACS Technical Report
%N 103
%@ false
%U http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_103.pdf
2015
Damm, W., Horbach, M., & Sofronie-Stokkermans, V. (2015). Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata (No. ATR111). SFB/TR 14 AVACS.
Export
BibTeX
@techreport{atr111,
TITLE = {Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata},
AUTHOR = {Damm, Werner and Horbach, Matthias and Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR111},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2015},
TYPE = {AVACS Technical Report},
VOLUME = {111},
}
Endnote
%0 Report
%A Damm, Werner
%A Horbach, Matthias
%A Sofronie-Stokkermans, Viorica
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002A-0805-6
%Y SFB/TR 14 AVACS
%D 2015
%P 52 p.
%B AVACS Technical Report
%N 111
%@ false
Schmidt, R. A., & Waldmann, U. (2015). Modal Tableau Systems with Blocking and Congruence Closure (No. uk-ac-man-scw:268816). Manchester: University of Manchester.
Export
BibTeX
@techreport{SchmidtTR2015,
TITLE = {Modal Tableau Systems with Blocking and Congruence Closure},
AUTHOR = {Schmidt, Renate A. and Waldmann, Uwe},
LANGUAGE = {eng},
NUMBER = {uk-ac-man-scw:268816},
INSTITUTION = {University of Manchester},
ADDRESS = {Manchester},
YEAR = {2015},
TYPE = {eScholar},
}
Endnote
%0 Report
%A Schmidt, Renate A.
%A Waldmann, Uwe
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Modal Tableau Systems with Blocking and Congruence Closure :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-002A-08BC-A
%Y University of Manchester
%C Manchester
%D 2015
%P 22 p.
%B eScholar
%U https://www.escholar.manchester.ac.uk/uk-ac-man-scw:268816https://www.research.manchester.ac.uk/portal/files/32297317/FULL_TEXT.PDF
2014
Horbach, M., & Sofronie-Stokkermans, V. (2014). Obtaining Finite Local Theory Axiomatizations via Saturation (No. ATR93). SFB/TR 14 AVACS.
Abstract
In this paper we study theory combinations over non-disjoint
signatures in which hierarchical and modular reasoning is
possible. We use a notion of locality of a theory extension
parameterized by a closure operator on ground terms.
We give criteria for recognizing these types of theory
extensions. We then show that combinations of extensions of
theories which are local in this extended sense have also a
locality property and hence allow modular and hierarchical
reasoning. We thus obtain parameterized decidability and
complexity results for many (combinations of) theories
important in verification.
Export
BibTeX
@techreport{atr093,
TITLE = {Obtaining Finite Local Theory Axiomatizations via Saturation},
AUTHOR = {Horbach, Matthias and Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR93},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2014},
ABSTRACT = {In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.},
TYPE = {AVACS Technical Report},
VOLUME = {93},
}
Endnote
%0 Report
%A Horbach, Matthias
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Obtaining Finite Local Theory Axiomatizations via Saturation :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0024-C90C-F
%Y SFB/TR 14 AVACS
%D 2014
%P 26 p.
%X In this paper we study theory combinations over non-disjoint
signatures in which hierarchical and modular reasoning is
possible. We use a notion of locality of a theory extension
parameterized by a closure operator on ground terms.
We give criteria for recognizing these types of theory
extensions. We then show that combinations of extensions of
theories which are local in this extended sense have also a
locality property and hence allow modular and hierarchical
reasoning. We thus obtain parameterized decidability and
complexity results for many (combinations of) theories
important in verification.
%B AVACS Technical Report
%N 93
%@ false
%U http://www.avacs.org/Publikationen/Open/avacs_technical_report_093.pdf
2013
Baumgartner, P., & Waldmann, U. (2013). Hierarchic Superposition with Weak Abstraction (No. MPI-I-2014-RG1-002). Saarbrücken: Max-Planck-Institut für Informatik.
Abstract
Many applications of automated deduction require reasoning in
first-order logic modulo background theories, in particular some
form of integer arithmetic. A major unsolved research challenge
is to design theorem provers that are "reasonably complete"
even in the presence of free function symbols ranging into a
background theory sort. The hierarchic superposition calculus
of Bachmair, Ganzinger, and Waldmann already supports such
symbols, but, as we demonstrate, not optimally. This paper aims
to rectify the situation by introducing a novel form of clause
abstraction, a core component in the hierarchic superposition
calculus for transforming clauses into a form needed for internal
operation. We argue for the benefits of the resulting calculus
and provide a new completeness result for the fragment where
all background-sorted terms are ground.
Export
BibTeX
@techreport{Waldmann2013,
TITLE = {Hierarchic Superposition with Weak Abstraction},
AUTHOR = {Baumgartner, Peter and Waldmann, Uwe},
LANGUAGE = {eng},
ISSN = {0946-011X},
NUMBER = {MPI-I-2014-RG1-002},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2013},
ABSTRACT = {Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even in the presence of free function symbols ranging into a background theory sort. The hierarchic superposition calculus of Bachmair, Ganzinger, and Waldmann already supports such symbols, but, as we demonstrate, not optimally. This paper aims to rectify the situation by introducing a novel form of clause abstraction, a core component in the hierarchic superposition calculus for transforming clauses into a form needed for internal operation. We argue for the benefits of the resulting calculus and provide a new completeness result for the fragment where all background-sorted terms are ground.},
TYPE = {Research Report},
}
Endnote
%0 Report
%A Baumgartner, Peter
%A Waldmann, Uwe
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Hierarchic Superposition with Weak Abstraction :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0024-03A8-0
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2013
%P 45 p.
%X Many applications of automated deduction require reasoning in
first-order logic modulo background theories, in particular some
form of integer arithmetic. A major unsolved research challenge
is to design theorem provers that are "reasonably complete"
even in the presence of free function symbols ranging into a
background theory sort. The hierarchic superposition calculus
of Bachmair, Ganzinger, and Waldmann already supports such
symbols, but, as we demonstrate, not optimally. This paper aims
to rectify the situation by introducing a novel form of clause
abstraction, a core component in the hierarchic superposition
calculus for transforming clauses into a form needed for internal
operation. We argue for the benefits of the resulting calculus
and provide a new completeness result for the fragment where
all background-sorted terms are ground.
%B Research Report
%@ false
2012
Fietzke, A., Kruglov, E., & Weidenbach, C. (2012). Automatic Generation of Invariants for Circular Derivations in SUP(LA) 1 (No. MPI-I-2012-RG1-002). Saarbrücken: Max-Planck-Institut für Informatik.
Abstract
The hierarchic combination of linear arithmetic and firstorder
logic with free function symbols, FOL(LA), results in a strictly
more expressive logic than its two parts. The SUP(LA) calculus can be
turned into a decision procedure for interesting fragments of FOL(LA).
For example, reachability problems for timed automata can be decided
by SUP(LA) using an appropriate translation into FOL(LA). In this paper,
we extend the SUP(LA) calculus with an additional inference rule,
automatically generating inductive invariants from partial SUP(LA)
derivations. The rule enables decidability of more expressive fragments,
including reachability for timed automata with unbounded integer variables.
We have implemented the rule in the SPASS(LA) theorem prover
with promising results, showing that it can considerably speed up proof
search and enable termination of saturation for practically relevant
problems.
Export
BibTeX
@techreport{FietzkeKruglovWeidenbach2012,
TITLE = {Automatic Generation of Invariants for Circular Derivations in {SUP(LA)} 1},
AUTHOR = {Fietzke, Arnaud and Kruglov, Evgeny and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0946-011X},
NUMBER = {MPI-I-2012-RG1-002},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2012},
ABSTRACT = {The hierarchic combination of linear arithmetic and firstorder logic with free function symbols, FOL(LA), results in a strictly more expressive logic than its two parts. The SUP(LA) calculus can be turned into a decision procedure for interesting fragments of FOL(LA). For example, reachability problems for timed automata can be decided by SUP(LA) using an appropriate translation into FOL(LA). In this paper, we extend the SUP(LA) calculus with an additional inference rule, automatically generating inductive invariants from partial SUP(LA) derivations. The rule enables decidability of more expressive fragments, including reachability for timed automata with unbounded integer variables. We have implemented the rule in the SPASS(LA) theorem prover with promising results, showing that it can considerably speed up proof search and enable termination of saturation for practically relevant problems.},
TYPE = {Research Report},
}
Endnote
%0 Report
%A Fietzke, Arnaud
%A Kruglov, Evgeny
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Automatic Generation of Invariants for Circular Derivations in SUP(LA) 1 :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0024-03CF-9
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2012
%P 26 p.
%X The hierarchic combination of linear arithmetic and firstorder
logic with free function symbols, FOL(LA), results in a strictly
more expressive logic than its two parts. The SUP(LA) calculus can be
turned into a decision procedure for interesting fragments of FOL(LA).
For example, reachability problems for timed automata can be decided
by SUP(LA) using an appropriate translation into FOL(LA). In this paper,
we extend the SUP(LA) calculus with an additional inference rule,
automatically generating inductive invariants from partial SUP(LA)
derivations. The rule enables decidability of more expressive fragments,
including reachability for timed automata with unbounded integer variables.
We have implemented the rule in the SPASS(LA) theorem prover
with promising results, showing that it can considerably speed up proof
search and enable termination of saturation for practically relevant
problems.
%B Research Report
%@ false
Suda, M., & Weidenbach, C. (2012). Labelled Superposition for PLTL (No. MPI-I-2012-RG1-001). Saarbrücken: Max-Planck-Institut für Informatik.
Abstract
This paper introduces a new decision procedure for PLTL based on labelled
superposition.
Its main idea is to treat temporal formulas as infinite sets of purely
propositional clauses over an extended signature. These infinite sets are then
represented by finite sets of labelled propositional clauses. The new
representation enables the replacement of the complex temporal resolution
rule, suggested by existing resolution calculi for PLTL, by a fine grained
repetition check of finitely saturated labelled clause sets followed by a
simple inference. The completeness argument is based on the standard model
building idea from superposition. It inherently justifies ordering
restrictions, redundancy elimination and effective partial model building. The
latter can be directly used to effectively generate counterexamples of
non-valid PLTL conjectures out of saturated labelled clause sets in a
straightforward way.
Export
BibTeX
@techreport{SudaWeidenbachLPAR2012,
TITLE = {Labelled Superposition for {PLTL}},
AUTHOR = {Suda, Martin and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0946-011X},
NUMBER = {MPI-I-2012-RG1-001},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2012},
ABSTRACT = {This paper introduces a new decision procedure for PLTL based on labelled superposition. Its main idea is to treat temporal formulas as infinite sets of purely propositional clauses over an extended signature. These infinite sets are then represented by finite sets of labelled propositional clauses. The new representation enables the replacement of the complex temporal resolution rule, suggested by existing resolution calculi for PLTL, by a fine grained repetition check of finitely saturated labelled clause sets followed by a simple inference. The completeness argument is based on the standard model building idea from superposition. It inherently justifies ordering restrictions, redundancy elimination and effective partial model building. The latter can be directly used to effectively generate counterexamples of non-valid PLTL conjectures out of saturated labelled clause sets in a straightforward way.},
TYPE = {Research Reports},
}
Endnote
%0 Report
%A Suda, Martin
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Labelled Superposition for PLTL :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0024-03DC-B
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2012
%P 42 p.
%X This paper introduces a new decision procedure for PLTL based on labelled
superposition.
Its main idea is to treat temporal formulas as infinite sets of purely
propositional clauses over an extended signature. These infinite sets are then
represented by finite sets of labelled propositional clauses. The new
representation enables the replacement of the complex temporal resolution
rule, suggested by existing resolution calculi for PLTL, by a fine grained
repetition check of finitely saturated labelled clause sets followed by a
simple inference. The completeness argument is based on the standard model
building idea from superposition. It inherently justifies ordering
restrictions, redundancy elimination and effective partial model building. The
latter can be directly used to effectively generate counterexamples of
non-valid PLTL conjectures out of saturated labelled clause sets in a
straightforward way.
%B Research Reports
%@ false
2011
Damm, W., Ihlemann, C., & Sofronie-Stokkermans, V. (2011). PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata (No. ATR70). SFB/TR 14 AVACS.
Abstract
This paper identifies an industrially relevant class of
linear hybrid automata (LHA) called reasonable LHA for
which parametric verification of convex safety properties
with exhaustive entry states can be verified in polynomial
time and time-bounded reachability can be decided
in nondeterministic polynomial time for non-parametric
verification and in exponential time for
parametric verification. Properties with exhaustive entry
states are restricted to runs originating in
a (specified) inner envelope of some mode-invariant.
Deciding whether an LHA is reasonable is
shown to be decidable in polynomial time.
Export
BibTeX
@techreport{Damm-Ihlemann-Sofronie-Stokkermans2011-report,
TITLE = {{PTIME} Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata},
AUTHOR = {Damm, Werner and Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR70},
LOCALID = {Local-ID: C125716C0050FB51-DEB90D4E9EAE27B7C1257855003AF8EE-Damm-Ihlemann-Sofronie-Stokkermans2011-report},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2011},
DATE = {2011},
ABSTRACT = {This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of convex safety properties with exhaustive entry states can be verified in polynomial time and time-bounded reachability can be decided in nondeterministic polynomial time for non-parametric verification and in exponential time for parametric verification. Properties with exhaustive entry states are restricted to runs originating in a (specified) inner envelope of some mode-invariant. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.},
TYPE = {AVACS Technical Report},
VOLUME = {70},
}
Endnote
%0 Report
%A Damm, Werner
%A Ihlemann, Carsten
%A Sofronie-Stokkermans, Viorica
%+ External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0010-14F5-F
%F EDOC: 619013
%F OTHER: Local-ID: C125716C0050FB51-DEB90D4E9EAE27B7C1257855003AF8EE-Damm-Ihlemann-Sofronie-Stokkermans2011-report
%Y SFB/TR 14 AVACS
%D 2011
%P 31 p.
%X This paper identifies an industrially relevant class of
linear hybrid automata (LHA) called reasonable LHA for
which parametric verification of convex safety properties
with exhaustive entry states can be verified in polynomial
time and time-bounded reachability can be decided
in nondeterministic polynomial time for non-parametric
verification and in exponential time for
parametric verification. Properties with exhaustive entry
states are restricted to runs originating in
a (specified) inner envelope of some mode-invariant.
Deciding whether an LHA is reasonable is
shown to be decidable in polynomial time.
%B AVACS Technical Report
%N 70
%@ false
%U http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_070.pdf
Damm, W., Disch, S., Hagemann, W., Scholl, C., Waldmann, U., & Wirtz, B. (2011). Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems (No. ATR76). (B. Becker, W. Damm, B. Finkbeiner, M. Fränzle, E.-R. Olderog, & A. Podelski, Eds.). Saarbrücken: SFB/TR 14 AVACS.
Abstract
We describe an approach to integrate incremental ow pipe computation into a
fully symbolic backward model checker for hybrid systems. Our method combines
the advantages of symbolic state set representation, such as the ability to
deal with large numbers of boolean variables, with an effcient way to handle
continuous ows dened by linear differential equations, possibly including
bounded disturbances.
Export
BibTeX
@techreport{DammDierksHagemannEtAl2011,
TITLE = {Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems},
AUTHOR = {Damm, Werner and Disch, Stefan and Hagemann, Willem and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
EDITOR = {Becker, Bernd and Damm, Werner and Finkbeiner, Bernd and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR76},
INSTITUTION = {SFB/TR 14 AVACS},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2011},
DATE = {2011},
ABSTRACT = {We describe an approach to integrate incremental ow pipe computation into a fully symbolic backward model checker for hybrid systems. Our method combines the advantages of symbolic state set representation, such as the ability to deal with large numbers of boolean variables, with an effcient way to handle continuous ows dened by linear differential equations, possibly including bounded disturbances.},
TYPE = {AVACS Technical Report},
VOLUME = {76},
}
Endnote
%0 Report
%A Damm, Werner
%A Disch, Stefan
%A Hagemann, Willem
%A Scholl, Christoph
%A Waldmann, Uwe
%A Wirtz, Boris
%E Becker, Bernd
%E Damm, Werner
%E Finkbeiner, Bernd
%E Fränzle, Martin
%E Olderog, Ernst-Rüdiger
%E Podelski, Andreas
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
External Organizations
%T Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-001A-150E-7
%Y SFB/TR 14 AVACS
%C Saarbrücken
%D 2011
%X We describe an approach to integrate incremental ow pipe computation into a
fully symbolic backward model checker for hybrid systems. Our method combines
the advantages of symbolic state set representation, such as the ability to
deal with large numbers of boolean variables, with an effcient way to handle
continuous ows dened by linear differential equations, possibly including
bounded disturbances.
%B AVACS Technical Report
%N 76
%@ false
Lu, T., Merz, S., & Weidenbach, C. (2011). Towards Verification of the Pastry Protocol using TLA+ (No. MPI-I-2011-RG1-002). Saarbrücken: Max-Planck-Institut für Informatik. Retrieved from http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2011-RG1-002
Abstract
Pastry is an algorithm that provides a scalable distributed hash table over
an underlying P2P network. Several implementations of Pastry are available
and have been applied in practice, but no attempt has so far been made to
formally describe the algorithm or to verify its properties. Since Pastry combines
rather complex data structures, asynchronous communication, concurrency,
resilience to churn and fault tolerance, it makes an interesting target
for verication. We have modeled Pastry's core routing algorithms and communication
protocol in the specication language TLA+. In order to validate
the model and to search for bugs we employed the TLA+ model checker tlc
to analyze several qualitative properties. We obtained non-trivial insights in
the behavior of Pastry through the model checking analysis. Furthermore,
we started to verify Pastry using the very same model and the interactive
theorem prover tlaps for TLA+. A rst result is the reduction of global
Pastry correctness properties to invariants of the underlying data structures.
Export
BibTeX
@techreport{LuMerzWeidenbach2011,
TITLE = {Towards Verification of the {Pastry} Protocol using {TLA+}},
AUTHOR = {Lu, Tianxiang and Merz, Stephan and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2011-RG1-002},
NUMBER = {MPI-I-2011-RG1-002},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2011},
DATE = {2011},
ABSTRACT = {Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verication. We have modeled Pastry's core routing algorithms and communication protocol in the specication language TLA+. In order to validate the model and to search for bugs we employed the TLA+ model checker tlc to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA+. A rst result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.},
TYPE = {Research Report},
}
Endnote
%0 Report
%A Lu, Tianxiang
%A Merz, Stephan
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Towards Verification of the Pastry Protocol using TLA+ :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-6975-A
%U http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2011-RG1-002
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2011
%P 51 p.
%X Pastry is an algorithm that provides a scalable distributed hash table over
an underlying P2P network. Several implementations of Pastry are available
and have been applied in practice, but no attempt has so far been made to
formally describe the algorithm or to verify its properties. Since Pastry combines
rather complex data structures, asynchronous communication, concurrency,
resilience to churn and fault tolerance, it makes an interesting target
for verication. We have modeled Pastry's core routing algorithms and communication
protocol in the specication language TLA+. In order to validate
the model and to search for bugs we employed the TLA+ model checker tlc
to analyze several qualitative properties. We obtained non-trivial insights in
the behavior of Pastry through the model checking analysis. Furthermore,
we started to verify Pastry using the very same model and the interactive
theorem prover tlaps for TLA+. A rst result is the reduction of global
Pastry correctness properties to invariants of the underlying data structures.
%B Research Report
2010
Faber, J., Ihlemann, C., Jacobs, S., & Sofronie-Stokkermans, V. (2010). Automatic Verification of Parametric Specifications with Complex Topologies (No. ATR66). SFB/TR 14 AVACS.
Abstract
The focus of this paper is on reducing the complexity in
verification by exploiting modularity at various levels:
in specification, in verification, and structurally.
\begin{itemize}
\item For specifications, we use the modular language CSP-OZ-DC,
which allows us to decouple verification tasks concerning
data from those concerning durations.
\item At the verification level, we exploit modularity in
theorem proving for rich data structures and use this for
invariant checking.
\item At the structural level, we analyze possibilities
for modular verification of systems consisting of various
components which interact.
\end{itemize}
We illustrate these ideas by automatically verifying safety
properties of a case study from the European Train Control
System standard, which extends previous examples by comprising a
complex track topology with lists of track segments and trains
with different routes.
Export
BibTeX
@techreport{faber-ihlemann-jacobs-sofronie-2010-report,
TITLE = {Automatic Verification of Parametric Specifications with Complex Topologies},
AUTHOR = {Faber, Johannes and Ihlemann, Carsten and Jacobs, Swen and Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR66},
LOCALID = {Local-ID: C125716C0050FB51-2E8AD7BA67FF4CB5C12577B4004D8EF8-faber-ihlemann-jacobs-sofronie-2010-report},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2010},
DATE = {2010},
ABSTRACT = {The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. \begin{itemize} \item For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. \item At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. \item At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. \end{itemize} We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.},
TYPE = {AVACS Technical Report},
VOLUME = {66},
}
Endnote
%0 Report
%A Faber, Johannes
%A Ihlemann, Carsten
%A Jacobs, Swen
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Automatic Verification of Parametric Specifications with Complex Topologies :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-14A6-8
%F EDOC: 536341
%F OTHER: Local-ID: C125716C0050FB51-2E8AD7BA67FF4CB5C12577B4004D8EF8-faber-ihlemann-jacobs-sofronie-2010-report
%Y SFB/TR 14 AVACS
%D 2010
%P 40 p.
%X The focus of this paper is on reducing the complexity in
verification by exploiting modularity at various levels:
in specification, in verification, and structurally.
\begin{itemize}
\item For specifications, we use the modular language CSP-OZ-DC,
which allows us to decouple verification tasks concerning
data from those concerning durations.
\item At the verification level, we exploit modularity in
theorem proving for rich data structures and use this for
invariant checking.
\item At the structural level, we analyze possibilities
for modular verification of systems consisting of various
components which interact.
\end{itemize}
We illustrate these ideas by automatically verifying safety
properties of a case study from the European Train Control
System standard, which extends previous examples by comprising a
complex track topology with lists of track segments and trains
with different routes.
%B AVACS Technical Report
%N 66
%@ false
Ihlemann, C., & Sofronie-Stokkermans, V. (2010a). On Hierarchical Reasoning in Combinations of Theories (No. ATR60). SFB/TR 14 AVACS.
Abstract
In this paper we study theory combinations over non-disjoint
signatures in which hierarchical and modular reasoning is
possible. We use a notion of locality of a theory extension
parameterized by a closure operator on ground terms.
We give criteria for recognizing these types of theory
extensions. We then show that combinations of extensions of
theories which are local in this extended sense have also a
locality property and hence allow modular and hierarchical
reasoning. We thus obtain parameterized decidability and
complexity results for many (combinations of) theories
important in verification.
Export
BibTeX
@techreport{Ihlemann-Sofronie-Stokkermans-atr60-2010,
TITLE = {On Hierarchical Reasoning in Combinations of Theories},
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR60},
LOCALID = {Local-ID: C125716C0050FB51-8E77AFE123C76116C1257782003FEBDA-Ihlemann-Sofronie-Stokkermans-atr60-2010},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2010},
DATE = {2010},
ABSTRACT = {In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.},
TYPE = {AVACS Technical Report},
VOLUME = {60},
}
Endnote
%0 Report
%A Ihlemann, Carsten
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T On Hierarchical Reasoning in Combinations of Theories :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-14B7-2
%F EDOC: 536339
%F OTHER: Local-ID: C125716C0050FB51-8E77AFE123C76116C1257782003FEBDA-Ihlemann-Sofronie-Stokkermans-atr60-2010
%Y SFB/TR 14 AVACS
%D 2010
%P 26 p.
%X In this paper we study theory combinations over non-disjoint
signatures in which hierarchical and modular reasoning is
possible. We use a notion of locality of a theory extension
parameterized by a closure operator on ground terms.
We give criteria for recognizing these types of theory
extensions. We then show that combinations of extensions of
theories which are local in this extended sense have also a
locality property and hence allow modular and hierarchical
reasoning. We thus obtain parameterized decidability and
complexity results for many (combinations of) theories
important in verification.
%B AVACS Technical Report
%N 60
%@ false
%U http://www.avacs.org/Publikationen/Open/avacs_technical_report_060.pdf
Ihlemann, C., & Sofronie-Stokkermans, V. (2010b). System Description: H-PILoT (Version 1.9) (No. ATR61). SFB/TR 14 AVACS.
Abstract
This system description provides an overview of H-PILoT
(Hierarchical Proving by Instantiation in Local Theory
extensions), a program for hierarchical reasoning in
extensions of logical theories.
H-PILoT reduces deduction problems in the theory extension
to deduction problems in the base theory.
Specialized provers and standard SMT solvers can be used
for testing the satisfiability of the formulae obtained
after the reduction. For a certain type of theory extension
(namely for {\em local theory extensions}) this
hierarchical reduction is sound and complete and --
if the formulae obtained this way belong to a fragment
decidable in the base theory -- H-PILoT provides a decision
procedure for testing satisfiability of ground formulae,
and can also be used for model generation.
Export
BibTeX
@techreport{Ihlemann-Sofronie-Stokkermans-atr61-2010,
TITLE = {System Description: H-{PILoT} (Version 1.9)},
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR61},
LOCALID = {Local-ID: C125716C0050FB51-5F53450808E13ED9C125778C00501AE6-Ihlemann-Sofronie-Stokkermans-atr61-2010},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2010},
DATE = {2010},
ABSTRACT = {This system description provides an overview of H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions), a program for hierarchical reasoning in extensions of logical theories. H-PILoT reduces deduction problems in the theory extension to deduction problems in the base theory. Specialized provers and standard SMT solvers can be used for testing the satisfiability of the formulae obtained after the reduction. For a certain type of theory extension (namely for {\em local theory extensions}) this hierarchical reduction is sound and complete and -- if the formulae obtained this way belong to a fragment decidable in the base theory -- H-PILoT provides a decision procedure for testing satisfiability of ground formulae, and can also be used for model generation.},
TYPE = {AVACS Technical Report},
VOLUME = {61},
}
Endnote
%0 Report
%A Ihlemann, Carsten
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T System Description: H-PILoT (Version 1.9) :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-14C5-2
%F EDOC: 536340
%F OTHER: Local-ID: C125716C0050FB51-5F53450808E13ED9C125778C00501AE6-Ihlemann-Sofronie-Stokkermans-atr61-2010
%Y SFB/TR 14 AVACS
%D 2010
%P 45 p.
%X This system description provides an overview of H-PILoT
(Hierarchical Proving by Instantiation in Local Theory
extensions), a program for hierarchical reasoning in
extensions of logical theories.
H-PILoT reduces deduction problems in the theory extension
to deduction problems in the base theory.
Specialized provers and standard SMT solvers can be used
for testing the satisfiability of the formulae obtained
after the reduction. For a certain type of theory extension
(namely for {\em local theory extensions}) this
hierarchical reduction is sound and complete and --
if the formulae obtained this way belong to a fragment
decidable in the base theory -- H-PILoT provides a decision
procedure for testing satisfiability of ground formulae,
and can also be used for model generation.
%B AVACS Technical Report
%N 61
%@ false
Suda, M., Weidenbach, C., & Wischnewski, P. (2010). On the saturation of YAGO (No. MPI-I-2010-RG1-001). Saarbrücken: Max-Planck-Institut für Informatik. Retrieved from http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2010-RG1-001
Export
BibTeX
@techreport{SudaWischnewski2010,
TITLE = {On the saturation of {YAGO}},
AUTHOR = {Suda, Martin and Weidenbach, Christoph and Wischnewski, Patrick},
LANGUAGE = {eng},
URL = {http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2010-RG1-001},
NUMBER = {MPI-I-2010-RG1-001},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2010},
DATE = {2010},
TYPE = {Research Report},
}
Endnote
%0 Report
%A Suda, Martin
%A Weidenbach, Christoph
%A Wischnewski, Patrick
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T On the saturation of YAGO :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-6584-2
%U http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2010-RG1-001
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2010
%P 50 p.
%B Research Report
2009
Horbach, M., & Weidenbach, C. (2009a). Deciding the Inductive Validity of Forall Exists* Queries (No. MPI-I-2009-RG1-001).
Abstract
We present a new saturation-based decidability result for inductive validity.
Let $\Sigma$ be a finite signature in which all function symbols are at most
unary and let $N$ be a satisfiable Horn clause set without equality in which
all positive literals are linear.
If $N\cup\{A_1,\ldots,A_n\rightarrow\}$ belongs to a finitely saturating clause
class, then it is decidable whether a sentence of the form $\forall\exists^*
(A_1\wedge\ldots\wedge A_n)$ is valid in the minimal model of $N$.
Export
BibTeX
@techreport{HorbachWeidenbach2009,
TITLE = {Deciding the Inductive Validity of Forall Exists* Queries},
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
LANGUAGE = {eng},
NUMBER = {MPI-I-2009-RG1-001},
LOCALID = {Local-ID: C125716C0050FB51-F9BA0666A42B8463C12576AF002882D7-Horbach2009TR1},
YEAR = {2009},
DATE = {2009},
ABSTRACT = {We present a new saturation-based decidability result for inductive validity. Let $\Sigma$ be a finite signature in which all function symbols are at most unary and let $N$ be a satisfiable Horn clause set without equality in which all positive literals are linear. If $N\cup\{A_1,\ldots,A_n\rightarrow\}$ belongs to a finitely saturating clause class, then it is decidable whether a sentence of the form $\forall\exists^* (A_1\wedge\ldots\wedge A_n)$ is valid in the minimal model of $N$.},
}
Endnote
%0 Report
%A Horbach, Matthias
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Deciding the Inductive Validity of Forall Exists* Queries :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-1A51-3
%F EDOC: 521099
%F OTHER: Local-ID: C125716C0050FB51-F9BA0666A42B8463C12576AF002882D7-Horbach2009TR1
%D 2009
%X We present a new saturation-based decidability result for inductive validity.
Let $\Sigma$ be a finite signature in which all function symbols are at most
unary and let $N$ be a satisfiable Horn clause set without equality in which
all positive literals are linear.
If $N\cup\{A_1,\ldots,A_n\rightarrow\}$ belongs to a finitely saturating clause
class, then it is decidable whether a sentence of the form $\forall\exists^*
(A_1\wedge\ldots\wedge A_n)$ is valid in the minimal model of $N$.
Horbach, M., & Weidenbach, C. (2009b). Superposition for Fixed Domains (No. MPI-I-2009-RG1-005). Saarbrücken: Max-Planck-Institut für Informatik.
Abstract
Superposition is an established decision procedure for a variety of first-order
logic theories represented by sets of clauses. A satisfiable theory, saturated
by superposition, implicitly defines a minimal term-generated model for the
theory.
Proving universal properties with respect to a saturated theory directly leads
to a modification of the minimal model's term-generated domain, as new Skolem
functions are introduced. For many applications, this is not desired.
Therefore, we propose the first superposition calculus that can explicitly
represent existentially quantified variables and can thus compute with respect
to a given domain. This calculus is sound and refutationally complete in the
limit for a first-order fixed domain semantics.
For saturated Horn theories and classes of positive formulas, we can even
employ the calculus to prove properties of the minimal model itself, going
beyond the scope of known superposition-based approaches.
Export
BibTeX
@techreport{Horbach2009TR2,
TITLE = {Superposition for Fixed Domains},
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0946-011X},
NUMBER = {MPI-I-2009-RG1-005},
LOCALID = {Local-ID: C125716C0050FB51-5DDBBB1B134360CFC12576AF0028D299-Horbach2009TR2},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2009},
DATE = {2009},
ABSTRACT = {Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and refutationally complete in the limit for a first-order fixed domain semantics. For saturated Horn theories and classes of positive formulas, we can even employ the calculus to prove properties of the minimal model itself, going beyond the scope of known superposition-based approaches.},
TYPE = {Research Report},
}
Endnote
%0 Report
%A Horbach, Matthias
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition for Fixed Domains :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-1A71-C
%F EDOC: 521100
%F OTHER: Local-ID: C125716C0050FB51-5DDBBB1B134360CFC12576AF0028D299-Horbach2009TR2
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2009
%P 49 p.
%X Superposition is an established decision procedure for a variety of first-order
logic theories represented by sets of clauses. A satisfiable theory, saturated
by superposition, implicitly defines a minimal term-generated model for the
theory.
Proving universal properties with respect to a saturated theory directly leads
to a modification of the minimal model's term-generated domain, as new Skolem
functions are introduced. For many applications, this is not desired.
Therefore, we propose the first superposition calculus that can explicitly
represent existentially quantified variables and can thus compute with respect
to a given domain. This calculus is sound and refutationally complete in the
limit for a first-order fixed domain semantics.
For saturated Horn theories and classes of positive formulas, we can even
employ the calculus to prove properties of the minimal model itself, going
beyond the scope of known superposition-based approaches.
%B Research Report
%@ false
Horbach, M., & Weidenbach, C. (2009c). Decidability Results for Saturation-based Model Building (No. MPI-I-2009-RG1-004). Saarbrücken: Max-Planck-Institut für Informatik. Retrieved from http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2009-RG1-004
Abstract
Saturation-based calculi such as superposition can be
successfully instantiated to decision procedures for many decidable
fragments of first-order logic. In case of termination without
generating an empty clause, a saturated clause set implicitly represents
a minimal model for all clauses, based on the underlying term ordering
of the superposition calculus. In general, it is not decidable whether a
ground atom, a clause or even a formula holds in this minimal model of a
satisfiable saturated clause set.
Based on an extension of our superposition calculus for fixed domains
with syntactic disequality constraints in a non-equational setting, we
describe models given by ARM (Atomic Representations of term Models) or
DIG (Disjunctions of Implicit Generalizations) representations as
minimal models of finite saturated clause sets. This allows us to
present several new decidability results for validity in such models.
These results extend in particular the known decidability results for
ARM and DIG representations.
Export
BibTeX
@techreport{HorbachWeidenbach2010,
TITLE = {Decidability Results for Saturation-based Model Building},
AUTHOR = {Horbach, Matthias and Weidenbach, Christoph},
LANGUAGE = {eng},
ISSN = {0946-011X},
URL = {http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2009-RG1-004},
NUMBER = {MPI-I-2009-RG1-004},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2009},
DATE = {2009},
ABSTRACT = {Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set. Based on an extension of our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting, we describe models given by ARM (Atomic Representations of term Models) or DIG (Disjunctions of Implicit Generalizations) representations as minimal models of finite saturated clause sets. This allows us to present several new decidability results for validity in such models. These results extend in particular the known decidability results for ARM and DIG representations.},
TYPE = {Research Report},
}
Endnote
%0 Report
%A Horbach, Matthias
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Decidability Results for Saturation-based Model Building :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-6659-B
%U http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2009-RG1-004
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2009
%P 38 p.
%X Saturation-based calculi such as superposition can be
successfully instantiated to decision procedures for many decidable
fragments of first-order logic. In case of termination without
generating an empty clause, a saturated clause set implicitly represents
a minimal model for all clauses, based on the underlying term ordering
of the superposition calculus. In general, it is not decidable whether a
ground atom, a clause or even a formula holds in this minimal model of a
satisfiable saturated clause set.
Based on an extension of our superposition calculus for fixed domains
with syntactic disequality constraints in a non-equational setting, we
describe models given by ARM (Atomic Representations of term Models) or
DIG (Disjunctions of Implicit Generalizations) representations as
minimal models of finite saturated clause sets. This allows us to
present several new decidability results for validity in such models.
These results extend in particular the known decidability results for
ARM and DIG representations.
%B Research Report
%@ false
Rybalchenko, A., & Sofronie-Stokkermans, V. (2009). Constraint Solving for Interpolation.
Export
BibTeX
@techreport{Rybalchenko-Sofronie-Stokkermans-2009,
TITLE = {Constraint Solving for Interpolation},
AUTHOR = {Rybalchenko, Andrey and Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
LOCALID = {Local-ID: C125716C0050FB51-7BE33255DCBCF2AAC1257650004B7C65-Rybalchenko-Sofronie-Stokkermans-2009},
YEAR = {2009},
DATE = {2009},
}
Endnote
%0 Report
%A Rybalchenko, Andrey
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Constraint Solving for Interpolation :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-1A4A-6
%F EDOC: 521091
%F OTHER: Local-ID: C125716C0050FB51-7BE33255DCBCF2AAC1257650004B7C65-Rybalchenko-Sofronie-Stokkermans-2009
%D 2009
Weidenbach, C., & Wischnewski, P. (2009). Contextual Rewriting (No. MPI-I-2009-RG1-002).
Export
BibTeX
@techreport{WischnewskiWeidenbach2009,
TITLE = {Contextual Rewriting},
AUTHOR = {Weidenbach, Christoph and Wischnewski, Patrick},
LANGUAGE = {eng},
NUMBER = {MPI-I-2009-RG1-002},
LOCALID = {Local-ID: C125716C0050FB51-DD89BAB0441DE797C125757F0034B8CB-WeidenbachWischnewskiReport2009},
YEAR = {2009},
DATE = {2009},
}
Endnote
%0 Report
%A Weidenbach, Christoph
%A Wischnewski, Patrick
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Contextual Rewriting :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-1A4C-2
%F EDOC: 521106
%F OTHER: Local-ID: C125716C0050FB51-DD89BAB0441DE797C125757F0034B8CB-WeidenbachWischnewskiReport2009
%D 2009
2008
Fietzke, A. L., & Weidenbach, C. (2008). Labelled splitting (No. MPI-I-2008-RG1-001). Saarbrücken: Max-Planck-Institut für Informatik. Retrieved from http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2008-RG1-001
Abstract
We define a superposition calculus with explicit splitting and
an explicit, new backtracking rule on the basis of labelled clauses.
For the first time we show a superposition calculus with explicit
backtracking rule sound and complete. The new backtracking rule advances
backtracking with branch condensing known from SPASS.
An experimental evaluation of an implementation of the new rule
shows that it improves considerably the
previous SPASS splitting implementation.
Finally, we discuss the relationship between labelled first-order
splitting and DPLL style splitting with intelligent backtracking
and clause learning.
Export
BibTeX
@techreport{FietzkeWeidenbach2008,
TITLE = {Labelled splitting},
AUTHOR = {Fietzke, Arnaud Luc and Weidenbach, Christoph},
LANGUAGE = {eng},
URL = {http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2008-RG1-001},
NUMBER = {MPI-I-2008-RG1-001},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2008},
DATE = {2008},
ABSTRACT = {We define a superposition calculus with explicit splitting and an explicit, new backtracking rule on the basis of labelled clauses. For the first time we show a superposition calculus with explicit backtracking rule sound and complete. The new backtracking rule advances backtracking with branch condensing known from SPASS. An experimental evaluation of an implementation of the new rule shows that it improves considerably the previous SPASS splitting implementation. Finally, we discuss the relationship between labelled first-order splitting and DPLL style splitting with intelligent backtracking and clause learning.},
TYPE = {Research Report},
}
Endnote
%0 Report
%A Fietzke, Arnaud Luc
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Labelled splitting :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-6674-D
%U http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2008-RG1-001
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2008
%P 45 p.
%X We define a superposition calculus with explicit splitting and
an explicit, new backtracking rule on the basis of labelled clauses.
For the first time we show a superposition calculus with explicit
backtracking rule sound and complete. The new backtracking rule advances
backtracking with branch condensing known from SPASS.
An experimental evaluation of an implementation of the new rule
shows that it improves considerably the
previous SPASS splitting implementation.
Finally, we discuss the relationship between labelled first-order
splitting and DPLL style splitting with intelligent backtracking
and clause learning.
%B Research Report
Sofronie-Stokkermans, V. (2008a). Efficient Hierarchical Reasoning about Functions over Numerical Domains (No. ATR45). SFB/TR 14 AVACS.
Abstract
We show that many properties studied in mathematical
analysis (monotonicity, boundedness, inverse, Lipschitz
properties, possibly combined with continuity or derivability)
are expressible by formulae in a class for which sound and
complete hierarchical proof methods for testing satisfiability of
sets of ground clauses exist.
The results are useful for automated reasoning in mathematical
analysis and for the verification of hybrid systems.
Export
BibTeX
@techreport{Sofronie-Stokkermans-atr45-2008,
TITLE = {Efficient Hierarchical Reasoning about Functions over Numerical Domains},
AUTHOR = {Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR45},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2008},
DATE = {2008},
ABSTRACT = {We show that many properties studied in mathematical analysis (monotonicity, boundedness, inverse, Lipschitz properties, possibly combined with continuity or derivability) are expressible by formulae in a class for which sound and complete hierarchical proof methods for testing satisfiability of sets of ground clauses exist. The results are useful for automated reasoning in mathematical analysis and for the verification of hybrid systems.},
TYPE = {AVACS Technical Report},
VOLUME = {45},
}
Endnote
%0 Report
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Efficient Hierarchical Reasoning about Functions over Numerical Domains :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0027-A46C-B
%Y SFB/TR 14 AVACS
%D 2008
%P 17 p.
%X We show that many properties studied in mathematical
analysis (monotonicity, boundedness, inverse, Lipschitz
properties, possibly combined with continuity or derivability)
are expressible by formulae in a class for which sound and
complete hierarchical proof methods for testing satisfiability of
sets of ground clauses exist.
The results are useful for automated reasoning in mathematical
analysis and for the verification of hybrid systems.
%B AVACS Technical Report
%N 45
%@ false
%U http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_045.pdf
Sofronie-Stokkermans, V. (2008b). Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems (No. ATR46). SFB/TR 14 AVACS.
Abstract
In this paper we show that states, transitions and behavior of
concurrent systems can often be modeled as sheaves over a
suitable topological space (where the topology expresses how the
interacting systems share the information). This allows us to use
results from categorical logic (and in particular geometric
logic) to describe which type of properties are transferred, if
valid locally in all component systems, also at a global level,
to the system obtained by interconnecting the individual systems.
The main area of application is to modular verification of
complex systems.
We illustrate the ideas by means of an example involving
a family of interacting controllers for trains on a rail track.
Export
BibTeX
@techreport{Sofronie-Stokkermans-atr46-2008,
TITLE = {Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems},
AUTHOR = {Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
ISSN = {1860-9821},
NUMBER = {ATR46},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2008},
DATE = {2008},
ABSTRACT = {In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space (where the topology expresses how the interacting systems share the information). This allows us to use results from categorical logic (and in particular geometric logic) to describe which type of properties are transferred, if valid locally in all component systems, also at a global level, to the system obtained by interconnecting the individual systems. The main area of application is to modular verification of complex systems. We illustrate the ideas by means of an example involving a family of interacting controllers for trains on a rail track.},
TYPE = {AVACS Technical Report},
VOLUME = {46},
}
Endnote
%0 Report
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0027-A579-5
%Y SFB/TR 14 AVACS
%D 2008
%X In this paper we show that states, transitions and behavior of
concurrent systems can often be modeled as sheaves over a
suitable topological space (where the topology expresses how the
interacting systems share the information). This allows us to use
results from categorical logic (and in particular geometric
logic) to describe which type of properties are transferred, if
valid locally in all component systems, also at a global level,
to the system obtained by interconnecting the individual systems.
The main area of application is to modular verification of
complex systems.
We illustrate the ideas by means of an example involving
a family of interacting controllers for trains on a rail track.
%B AVACS Technical Report
%N 46
%@ false
%U http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_046.pdf
2007
Hillenbrand, T., & Weidenbach, C. (2007). Superposition for Finite Domains (No. MPI-I-2007-RG1-002). Saarbrücken, Germany: Max-Planck-Institut für Informatik.
Export
BibTeX
@techreport{HillenbrandWeidenbach2007,
TITLE = {Superposition for Finite Domains},
AUTHOR = {Hillenbrand, Thomas and Weidenbach, Christoph},
LANGUAGE = {eng},
NUMBER = {MPI-I-2007-RG1-002},
LOCALID = {Local-ID: C12573CC004A8E26-1CF84BA6556F8748C12572C1002F229B-HillenbrandWeidenbach2007Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken, Germany},
YEAR = {2007},
DATE = {2007},
TYPE = {Max-Planck-Institut für Informatik / Research Report},
}
Endnote
%0 Report
%A Hillenbrand, Thomas
%A Weidenbach, Christoph
%+ Automation of Logic, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition for Finite Domains :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-000F-20DA-8
%F EDOC: 356455
%F OTHER: Local-ID: C12573CC004A8E26-1CF84BA6556F8748C12572C1002F229B-HillenbrandWeidenbach2007Report
%Y Max-Planck-Institut für Informatik
%C Saarbrücken, Germany
%D 2007
%P 25 p.
%B Max-Planck-Institut für Informatik / Research Report
2001
Sofronie-Stokkermans, V. (2001). Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators (No. MPI-I-2001-2-005). Saarbrücken: Max-Planck-Institut für Informatik. Retrieved from http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2001-2-005
Abstract
In this paper we establish a link between satisfiability of universal
sentences with respect to classes of distributive lattices with operators and
satisfiability with respect to certain classes of relational structures.
This justifies a method for structure-preserving translation to clause form
of universal (Horn) sentences in such classes of algebras.
We show that refinements of resolution yield decision procedures
for the universal (Horn) theory of some such classes.
In particular, we obtain exponential decision procedures
for the universal Horn theory of
(i) the class of all bounded distributive lattices with operators,
(ii) for the class of all bounded distributive lattices with operators
satisfying a set of (generalized) residuation conditions,
and a doubly-exponential decision procedure for the universal Horn theory of
the class of all Heyting algebras.
Export
BibTeX
@techreport{Sofronie-Stokkermans2001,
TITLE = {Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators},
AUTHOR = {Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
URL = {http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2001-2-005},
NUMBER = {MPI-I-2001-2-005},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2001},
DATE = {2001},
ABSTRACT = {In this paper we establish a link between satisfiability of universal sentences with respect to classes of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. This justifies a method for structure-preserving translation to clause form of universal (Horn) sentences in such classes of algebras. We show that refinements of resolution yield decision procedures for the universal (Horn) theory of some such classes. In particular, we obtain exponential decision procedures for the universal Horn theory of (i) the class of all bounded distributive lattices with operators, (ii) for the class of all bounded distributive lattices with operators satisfying a set of (generalized) residuation conditions, and a doubly-exponential decision procedure for the universal Horn theory of the class of all Heyting algebras.},
TYPE = {Research Report / Max-Planck-Institut für Informatik},
}
Endnote
%0 Report
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-6CB3-4
%U http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2001-2-005
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2001
%P 41 p.
%X In this paper we establish a link between satisfiability of universal
sentences with respect to classes of distributive lattices with operators and
satisfiability with respect to certain classes of relational structures.
This justifies a method for structure-preserving translation to clause form
of universal (Horn) sentences in such classes of algebras.
We show that refinements of resolution yield decision procedures
for the universal (Horn) theory of some such classes.
In particular, we obtain exponential decision procedures
for the universal Horn theory of
(i) the class of all bounded distributive lattices with operators,
(ii) for the class of all bounded distributive lattices with operators
satisfying a set of (generalized) residuation conditions,
and a doubly-exponential decision procedure for the universal Horn theory of
the class of all Heyting algebras.
%B Research Report / Max-Planck-Institut für Informatik
Waldmann, U. (2001). Superposition and chaining for totally ordered divisible abelian groups (No. MPI-I-2001-2-001). Saarbrücken: Max-Planck-Institut für Informatik.
Abstract
We present a calculus for first-order theorem proving in the
presence of the axioms of totally ordered divisible abelian groups.
The calculus extends previous superposition or chaining calculi for
divisible torsion-free abelian groups and dense total orderings
without endpoints. As its predecessors, it is refutationally
complete and requires neither explicit inferences with the theory
axioms nor variable overlaps. It offers thus an efficient way of
treating equalities and inequalities between additive terms over,
e.g., the rational numbers within a first-order theorem prover.
Export
BibTeX
@techreport{WaldmannMPI-I-2001-2-001,
TITLE = {Superposition and chaining for totally ordered divisible abelian groups},
AUTHOR = {Waldmann, Uwe},
LANGUAGE = {eng},
NUMBER = {MPI-I-2001-2-001},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {2001},
DATE = {2001},
ABSTRACT = {We present a calculus for first-order theorem proving in the presence of the axioms of totally ordered divisible abelian groups. The calculus extends previous superposition or chaining calculi for divisible torsion-free abelian groups and dense total orderings without endpoints. As its predecessors, it is refutationally complete and requires neither explicit inferences with the theory axioms nor variable overlaps. It offers thus an efficient way of treating equalities and inequalities between additive terms over, e.g., the rational numbers within a first-order theorem prover.},
TYPE = {Research Report / Max-Planck-Institut für Informatik},
}
Endnote
%0 Report
%A Waldmann, Uwe
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Superposition and chaining for totally ordered divisible abelian groups :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-6CFF-D
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 2001
%P 40 p.
%X We present a calculus for first-order theorem proving in the
presence of the axioms of totally ordered divisible abelian groups.
The calculus extends previous superposition or chaining calculi for
divisible torsion-free abelian groups and dense total orderings
without endpoints. As its predecessors, it is refutationally
complete and requires neither explicit inferences with the theory
axioms nor variable overlaps. It offers thus an efficient way of
treating equalities and inequalities between additive terms over,
e.g., the rational numbers within a first-order theorem prover.
%B Research Report / Max-Planck-Institut für Informatik
1999
Waldmann, U. (1999). Cancellative superposition decides the theory of divisible torsion-free abelian groups (No. MPI-I-1999-2-003). Saarbrücken: Max-Planck-Institut für Informatik.
Abstract
In divisible torsion-free abelian groups, the efficiency of the
cancellative superposition calculus can be greatly increased by
combining it with a variable elimination algorithm that transforms
every clause into an equivalent clause without unshielded variables.
We show that the resulting calculus is a decision procedure for
the theory of divisible torsion-free abelian groups.
Export
BibTeX
@techreport{WaldmannMPI-I-1999-2-003,
TITLE = {Cancellative superposition decides the theory of divisible torsion-free abelian groups},
AUTHOR = {Waldmann, Uwe},
LANGUAGE = {eng},
NUMBER = {MPI-I-1999-2-003},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {1999},
DATE = {1999},
ABSTRACT = {In divisible torsion-free abelian groups, the efficiency of the cancellative superposition calculus can be greatly increased by combining it with a variable elimination algorithm that transforms every clause into an equivalent clause without unshielded variables. We show that the resulting calculus is a decision procedure for the theory of divisible torsion-free abelian groups.},
TYPE = {Research Report / Max-Planck-Institut für Informatik},
}
Endnote
%0 Report
%A Waldmann, Uwe
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Cancellative superposition decides the theory of divisible torsion-free abelian groups :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-6F75-5
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 1999
%P 23 p.
%X In divisible torsion-free abelian groups, the efficiency of the
cancellative superposition calculus can be greatly increased by
combining it with a variable elimination algorithm that transforms
every clause into an equivalent clause without unshielded variables.
We show that the resulting calculus is a decision procedure for
the theory of divisible torsion-free abelian groups.
%B Research Report / Max-Planck-Institut für Informatik
1998
Sofronie-Stokkermans, V. (1998). Resolution-based Theorem Proving for SHn-Logics (No. E1852-GS-981). Vienna, Austria: Technische Universität Wien.
Abstract
In this paper we illustrate by means of an example, namely SHn-logics,
a method for translation to clause form and automated theorem proving for
first-order many-valued logics based on distributive lattices with operators.
Export
BibTeX
@techreport{Sofronie1998b,
TITLE = {Resolution-based Theorem Proving for {SH}n-Logics},
AUTHOR = {Sofronie-Stokkermans, Viorica},
LANGUAGE = {eng},
NUMBER = {E1852-GS-981},
INSTITUTION = {Technische Universit{\"a}t Wien},
ADDRESS = {Vienna, Austria},
YEAR = {1998},
DATE = {1998},
ABSTRACT = {In this paper we illustrate by means of an example, namely SHn-logics, a method for translation to clause form and automated theorem proving for first-order many-valued logics based on distributive lattices with operators.},
}
Endnote
%0 Report
%A Sofronie-Stokkermans, Viorica
%+ Automation of Logic, MPI for Informatics, Max Planck Society
%T Resolution-based Theorem Proving for SHn-Logics :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-001A-21C5-8
%Y Technische Universität Wien
%C Vienna, Austria
%D 1998
%X In this paper we illustrate by means of an example, namely SHn-logics,
a method for translation to clause form and automated theorem proving for
first-order many-valued logics based on distributive lattices with operators.
1996
Hähnle, R., Kerber, M., & Weidenbach, C. (1996). Common Syntax of the DFG-Schwerpunktprogramm Deduktion’' (No. 10/96). Karlsruhe: Universität Karlsruhe.
Export
BibTeX
@techreport{HaehnleKerberEtAl96,
TITLE = {Common Syntax of the {DFG-Schwerpunktprogramm} ''Deduktion''},
AUTHOR = {H{\"a}hnle, Reiner and Kerber, Manfred and Weidenbach, Christoph},
LANGUAGE = {eng},
NUMBER = {10/96},
INSTITUTION = {Universit{\"a}t Karlsruhe},
ADDRESS = {Karlsruhe},
YEAR = {1996},
DATE = {1996},
}
Endnote
%0 Report
%A Hähnle, Reiner
%A Kerber, Manfred
%A Weidenbach, Christoph
%+ External Organizations
External Organizations
Automation of Logic, MPI for Informatics, Max Planck Society
%T Common Syntax of the DFG-Schwerpunktprogramm ''Deduktion'' :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-001A-1CDF-C
%Y Universität Karlsruhe
%C Karlsruhe
%D 1996
1993
Bachmair, L., Ganzinger, H., Lynch, C., & Snyder, W. (1993). Basic paramodulation (No. MPI-I-93-236). Saarbrücken: Max-Planck-Institut für Informatik. Retrieved from http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/93-236
Abstract
We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the {\em basic\/} strategy for narrowing), in which paramodulation inferences are forbidden at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences.
Export
BibTeX
@techreport{Bachmair-et-el-93-mpii236,
TITLE = {Basic paramodulation},
AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Lynch, Christopher and Snyder, Wayne},
LANGUAGE = {eng},
URL = {http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/93-236},
NUMBER = {MPI-I-93-236},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Saarbr{\"u}cken},
YEAR = {1993},
DATE = {1993},
ABSTRACT = {We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the {\em basic\/} strategy for narrowing), in which paramodulation inferences are forbidden at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences.},
TYPE = {Research Report / Max-Planck-Institut für Informatik},
}
Endnote
%0 Report
%A Bachmair, Leo
%A Ganzinger, Harald
%A Lynch, Christopher
%A Snyder, Wayne
%+ Programming Logics, MPI for Informatics, Max Planck Society
Programming Logics, MPI for Informatics, Max Planck Society
Automation of Logic, MPI for Informatics, Max Planck Society
External Organizations
%T Basic paramodulation :
%G eng
%U http://hdl.handle.net/11858/00-001M-0000-0014-AAD5-4
%U http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/93-236
%Y Max-Planck-Institut für Informatik
%C Saarbrücken
%D 1993
%P 36 p.
%X We introduce a class of restrictions for the ordered paramodulation and superposition calculi (inspired by the {\em basic\/} strategy for narrowing), in which paramodulation inferences are forbidden at terms introduced by substitutions from previous inference steps. In addition we introduce restrictions based on term selection rules and redex orderings, which are general criteria for delimiting the terms which are available for inferences. These refinements are compatible with standard ordering restrictions and are complete without paramodulation into variables or using functional reflexivity axioms. We prove refutational completeness in the context of deletion rules, such as simplification by rewriting (demodulation) and subsumption, and of techniques for eliminating redundant inferences.
%B Research Report / Max-Planck-Institut für Informatik