HTTP/2 302
content-type: text/plain; charset=utf-8
date: Wed, 04 Feb 2026 04:02:00 GMT
location: https://oadoi.org/10.1007/3-540-45654-6_39
nel: {"report_to":"heroku-nel","response_headers":["Via"],"max_age":3600,"success_fraction":0.01,"failure_fraction":0.1}
report-to: {"group":"heroku-nel","endpoints":[{"url":"https://nel.heroku.com/reports?s=sE02HiGunbKYiG%2BVWY%2FjFS3saQuygNq6G7Iu3txqVlc%3D\u0026sid=67ff5de4-ad2b-4112-9289-cf96be89efed\u0026ts=1770177720"}],"max_age":3600}
reporting-endpoints: heroku-nel="https://nel.heroku.com/reports?s=sE02HiGunbKYiG%2BVWY%2FjFS3saQuygNq6G7Iu3txqVlc%3D&sid=67ff5de4-ad2b-4112-9289-cf96be89efed&ts=1770177720"
server: Heroku
vary: Accept
via: 2.0 heroku-router
x-powered-by: Express
content-length: 63
HTTP/1.1 302 Found
Access-Control-Allow-Headers: origin, content-type, accept, x-requested-with
Access-Control-Allow-Methods: POST, GET, OPTIONS, PUT, DELETE, PATCH
Access-Control-Allow-Origin: *
Content-Length: 291
Content-Security-Policy: default-src 'self'; object-src 'none'
Content-Type: text/html; charset=utf-8
Date: Wed, 04 Feb 2026 04:02:00 GMT
Location: https://oadoi.org/10.1007/3-540-45654-6_39
Nel: {"report_to":"heroku-nel","response_headers":["Via"],"max_age":3600,"success_fraction":0.01,"failure_fraction":0.1}
Referrer-Policy: strict-origin-when-cross-origin
Report-To: {"group":"heroku-nel","endpoints":[{"url":"https://nel.heroku.com/reports?s=HNp1A4LuLXc2L%2B9rO6kmP3fASt5Hxq8AEHIXSwWQudE%3D\u0026sid=929419e7-33ea-4e2f-85f0-7d8b7cd5cbd6\u0026ts=1770177720"}],"max_age":3600}
Reporting-Endpoints: heroku-nel="https://nel.heroku.com/reports?s=HNp1A4LuLXc2L%2B9rO6kmP3fASt5Hxq8AEHIXSwWQudE%3D&sid=929419e7-33ea-4e2f-85f0-7d8b7cd5cbd6&ts=1770177720"
Server: Heroku
Via: 1.1 heroku-router
X-Content-Type-Options: nosniff
X-Frame-Options: SAMEORIGIN
X-Xss-Protection: 1; mode=block
HTTP/2 302
access-control-allow-headers: origin, content-type, accept, x-requested-with
access-control-allow-methods: POST, GET, OPTIONS, PUT, DELETE, PATCH
access-control-allow-origin: *
content-security-policy: default-src 'self'; object-src 'none'
content-type: text/html; charset=utf-8
date: Wed, 04 Feb 2026 04:02:01 GMT
location: https://doi.org/10.1007/3-540-45654-6_39
nel: {"report_to":"heroku-nel","response_headers":["Via"],"max_age":3600,"success_fraction":0.01,"failure_fraction":0.1}
referrer-policy: strict-origin-when-cross-origin
report-to: {"group":"heroku-nel","endpoints":[{"url":"https://nel.heroku.com/reports?s=48FIxQgVd06V%2B0VfaXlUh82utUlsbSEZD9AbLpBmbvQ%3D\u0026sid=929419e7-33ea-4e2f-85f0-7d8b7cd5cbd6\u0026ts=1770177721"}],"max_age":3600}
reporting-endpoints: heroku-nel="https://nel.heroku.com/reports?s=48FIxQgVd06V%2B0VfaXlUh82utUlsbSEZD9AbLpBmbvQ%3D&sid=929419e7-33ea-4e2f-85f0-7d8b7cd5cbd6&ts=1770177721"
server: Heroku
strict-transport-security: max-age=31556926; includeSubDomains
via: 2.0 heroku-router
x-content-type-options: nosniff
x-frame-options: SAMEORIGIN
x-xss-protection: 1; mode=block
content-length: 285
HTTP/1.1 301 Moved Permanently
Date: Wed, 04 Feb 2026 04:02:01 GMT
Content-Length: 0
Connection: keep-alive
Location: https://doi.org/10.1007/3-540-45654-6_39
Report-To: {"group":"cf-nel","max_age":604800,"endpoints":[{"url":"https://a.nel.cloudflare.com/report/v4?s=7pmEw5pxQyDYZIa9wkHRNc%2FxhjUWqmQPeiD6wWACeTdqSPUzuJ7Lcgvw9BMB6AaQV7HTGFIz7q78WE7CFzSlRlGioCSbkg%3D%3D"}]}
Nel: {"report_to":"cf-nel","success_fraction":0.0,"max_age":604800}
Server: cloudflare
CF-RAY: 9c874528db06af3d-BLR
alt-svc: h3=":443"; ma=86400
HTTP/2 302
date: Wed, 04 Feb 2026 04:02:02 GMT
content-type: text/html;charset=utf-8
location: https://link.springer.com/10.1007/3-540-45654-6_39
server: cloudflare
vary: Origin
vary: Accept
expires: Wed, 04 Feb 2026 04:08:10 GMT
permissions-policy: interest-cohort=(),browsing-topics=()
cf-cache-status: DYNAMIC
nel: {"report_to":"cf-nel","success_fraction":0.0,"max_age":604800}
strict-transport-security: max-age=31536000; includeSubDomains; preload
report-to: {"group":"cf-nel","max_age":604800,"endpoints":[{"url":"https://a.nel.cloudflare.com/report/v4?s=2jBhnBsO5FdRDNz5mUug%2BpAN08E%2FesB8Zmqq8lftG66ZUTmEdj6sPCWFF5BsNc87%2BdU%2BY4zblY4zYCfMk8t30TdXjXCSiA%3D%3D"}]}
cf-ray: 9c8745291b696cd6-BLR
alt-svc: h3=":443"; ma=86400
HTTP/1.1 301 Moved Permanently
Connection: keep-alive
Content-Length: 166
location: https://link.springer.com/chapter/10.1007/3-540-45654-6_39
x-vcap-request-id: 122d7a5e-af6c-4a12-6182-a169edbc1caa
referrer-policy: no-referrer-when-downgrade
server: Oscar Platform 0.1581.0
cache-control: public,max-age=600
content-type: text/html
via: 1.1 google, 1.1 varnish
Accept-Ranges: bytes
Age: 0
Date: Wed, 04 Feb 2026 04:02:02 GMT
X-Served-By: cache-bom-vanm7210070-BOM, cache-bom-vanm7210055-BOM
X-Cache: MISS, MISS
X-Cache-Hits: 0, 0
X-Timer: S1770177722.094591,VS0,VE399
Vary: x-forwarded-host, upgrade-insecure-requests, x-forwarded-proto
alt-svc: h3=":443";ma=86400,h3-29=":443";ma=86400,h3-27=":443";ma=86400
HTTP/2 303
x-dump-request-bodies: 0
tracestate: gorouter=02aa460eade5cf66
x-vcap-request-id: 23664813-8373-4d52-7db9-65c01a8d7d44
via: 1.1 google, 1.1 varnish
x-b3-spanid: 1364939cf7316043
set-cookie: sim-inst-token="1::1770207722892:3ed75a4c"; Domain=.springer.com; Path=/; secure; HttpOnly
set-cookie: trackid="oeu2iojuq2f7brdikalcaerjo"; Domain=.springer.com; Path=/; secure; HttpOnly
age: 0
traceparent: 00-2366481383734d527db965c01a8d7d44-89d12baad3730a16-01
cache-control: no-cache
server: Oscar Platform 0.1581.0
x-b3-sampled: 1
x-b3-traceid: 335b45aca4555703
location: https://idp.springer.com/authorize?response_type=cookie&client_id=springerlink&redirect_uri=https%3A%2F%2Flink.springer.com%2Fchapter%2F10.1007%2F3-540-45654-6_39
x-frame-options: DENY
accept-ranges: bytes
date: Wed, 04 Feb 2026 04:02:03 GMT
x-served-by: cache-bom-vanm7210089-BOM, cache-bom-vanm7210058-BOM
x-cache: MISS, MISS, MISS
x-cache-hits: 0, 0
x-timer: S1770177723.555961,VS0,VE528
vary: x-frame-options,X-Oscar-Cache-Mode
alt-svc: h3=":443";ma=86400,h3-29=":443";ma=86400,h3-27=":443";ma=86400
content-length: 0
HTTP/2 302
cache-control: no-cache, no-store, max-age=0, must-revalidate
content-security-policy: frame-ancestors 'none';
expires: 0
location: https://link.springer.com/chapter/10.1007/3-540-45654-6_39
pragma: no-cache
set-cookie: idp_session=sVERSION_1f41f0446-b98b-48c7-9592-b5862e3ff345; Domain=.springer.com; Path=/; Secure; SameSite=None; HttpOnly
set-cookie: idp_session_http=hVERSION_10e9b0d50-d127-40f0-a5d2-08d09ec1928d; Domain=.springer.com; Path=/; HttpOnly
set-cookie: idp_marker=1d31d849-ad32-439d-b823-78184f58aed5; Domain=.springer.com; Path=/; Max-Age=34560000; HttpOnly
strict-transport-security: max-age=31536000 ; includeSubDomains
traceparent: 00-38fe9091af5e42727988a6ae485cde36-686cf693ed0815fa-01
x-content-type-options: nosniff
x-frame-options: DENY
x-vcap-request-id: 38fe9091-af5e-4272-7988-a6ae485cde36
x-xss-protection: 1; mode=block
via: 1.1 google, 1.1 varnish
x-cdn-origin: SNPaaS
accept-ranges: bytes
date: Wed, 04 Feb 2026 04:02:03 GMT
x-served-by: cache-bom-vanm7210066-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1770177723.143228,VS0,VE368
vary: x-forwarded-proto
alt-svc: h3=":443";ma=86400,h3-29=":443";ma=86400,h3-27=":443";ma=86400
content-length: 0
HTTP/2 200
traceparent: 00-5970a0b0b6d5488e424c42122779f086-a850bda252d6acda-01
via: 1.1 google, 1.1 varnish
accept-ranges: bytes
x-vcap-request-id: 5970a0b0-b6d5-488e-424c-42122779f086
x-dump-request-bodies: 0
content-encoding: gzip
age: 0
x-frame-options: DENY
x-b3-sampled: 1
content-type: text/html; charset=utf-8
x-b3-traceid: d88111405599d6c9
server: Oscar Platform 0.1581.0
x-b3-spanid: e0a2664d4482e1ae
set-cookie: sim-inst-token="1::1770207722892:3ed75a4c"; Domain=.springer.com; Path=/; secure; HttpOnly
set-cookie: user.uuid.v2="440512e0-11c4-48b1-b6d3-c74d3649d72e"; Expires=Mon, 04 May 2026 04:02:03 GMT; Domain=.springer.com; Path=/; secure; HttpOnly
tracestate: gorouter=3e8c6c72df99ce23
etag: "e36e77a39b0f431217b4ba37d702f134"
date: Wed, 04 Feb 2026 04:02:04 GMT
x-served-by: cache-bom-vanm7210089-BOM, cache-bom-vanm7210058-BOM
x-cache: MISS, MISS, MISS
x-cache-hits: 0, 0
x-timer: S1770177724.526053,VS0,VE821
vary: x-frame-options,X-Oscar-Cache-Mode, Accept-Encoding
alt-svc: h3=":443";ma=86400,h3-29=":443";ma=86400,h3-27=":443";ma=86400
Classifying Isomorphic Residue Classes | Springer Nature Link
Skip to main content
Included in the following conference series:
Abstract We report on a case study on combining proof planning with computer algebra systems. We construct proofs for basic algebraic properties of residue classes as well as for isomorphisms between residue classes using different proving techniques, which are implemented as strategies in a multi-strategy proof planner. We show how these techniques help to successfully derive proofs in our domain and explain how the search space of the proof planner can be drastically reduced by employing computations of two computer algebra systems during the planning process. Moreover, we discuss the results of experiments we conducted which give evidence that with the help of the computer algebra systems the planner is able to solve problems for which it would fail to create a proof otherwise.
The author’s work was supported by the ‘Graduiertenförderung des Saarlandes’.
The author’s work was supported by the’ studienstiftung des Deutschen Volkes’.
Similar content being viewed by others
References A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In Proceedings of CADE-9 , volume 310 of LNCS . Springer, 1988.
Google Scholar
C. Benzmüuller et al. ΩMega: Towards a Mathematical Assistant. In Proceedings of CADE-14 , volume 1249 of LNAI . Springer, 1997.
Google Scholar
E. Melis et al. ActiveMath system description. In Artificial Intelligence and Education , 2001.
Google Scholar
M. Fujita, J. Slaney, and F. Bennett. Automatic generation of some results in finite algebra. In Proceedings of IJCAI’93 . Morgan Kaufmann, 1993.
Google Scholar
The GAP Group. GAP-Groups, Algorithms, and Programming, Version 4 , 1998. https://www-gap.dcs.st-and.ac.uk/~{gap} .
C. Gomes, B. Selman, and H. Kautz. Boosting combinatorial search through randomization. In Proceedings of AAAI-98 . AAAI Press, 1998.
Google Scholar
P. Jackson. Exploring Abstract Algebra in Constructive Type Theory. In Proceedings of CADE-12 , volume 814 of LNCS . Springer, 1994.
Google Scholar
D. Kapur and D. Wang, editors. Journal of Automated Reasoning— Special Issue on the Integration of Deduction and Symbolic Computation Systems , volume 21(3). Kluwer Academic Publisher, 1998.
Google Scholar
Google Scholar
M. Kerber, M. Kohlhase, and V. Sorge. Integrating Computer Algebra Into Proof Planning. Journal of Automated Reasoning , 21(3), 1998.
Google Scholar
W. McCune. Otter 3.0 Reference Manual and Guide. Technical Report ANL-94-6, Argonne National Laboratory, Argonne, IL, USA, 1994.
Google Scholar
A. Meier. Randomization and heavy-tailed behavior in proof planning. Seki Report SR-00-03, Fachbereich Informatik, Universität des Saarlandes, 2000.
Google Scholar
A. Meier, M. Pollet, and V. Sorge. Exploring the domain of residue classes. Seki Report SR-00-04, Fachbereich Informatik, Universitäat des Saarlandes, 2000.
Google Scholar
A. Meier and V. Sorge. Exploring Properties of Residue Classes. In Proceedings of Calculemus 2000 . AK Peters, 2001.
Google Scholar
E. Melis and A. Meier. Proof planning with multiple strategies. In Proc. of the First International Conference on Computational Logic . Springer, 2000.
Google Scholar
E. Melis and J. Siekmann. Knowledge-based proof planning. Artificial Intelligence , 115(1), 1999.
Google Scholar
D. Redfern. The Maple Handbook: Maple V Release 5 . Springer, 1999.
Google Scholar
J. Slaney, M. Fujita, and M. Stickel. Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications , 29, 1995.
Google Scholar
V. Sorge. Non-Trivial Computations in Proof Planning. In Proceedings of FroCoS 2000 , volume 1794 of LNCS . Springer, 2000.
Google Scholar
Z. Zilic and K. Radecka. On feasible multivariate polynomial interpolations over arbitrary fields. In Proceedings of ISSAC-99 . ACM Press, 1999.
Google Scholar
R. Zippel. Interpolating polynomials from their values. Journal of Symbolic Computation , 9(3), 1990.
Google Scholar
Download references
Author information Authors and Affiliations Fachbereich Informatik, Universität des Saarlandes, Germany
Andreas Meier, Martin Pollet & Volker Sorge
Authors Andreas Meier Martin Pollet Volker Sorge Editor information Editors and Affiliations Universidad de Las Palmas de Gran Canaria, Instituto Universitario de Ciencias y Tecnologías Cibernéticas, Campus de Tafira, 35017, Las Palmas de Gran Canaria, Spain
Roberto Moreno-Díaz
University of Linz, Research Institute for Symbolic Computation, 232, Schloss Hagenberg, Austria
Bruno Buchberger
University ofA Coruña, Facultad de Informática, LFCIA, Dpto. of Computer Science, Campus de Elviña, 15071, A Coruña, Spain
José Luis Freire
Copyright information © 2001 Springer-Verlag Berlin Heidelberg
