BEGIN:VCALENDAR VERSION:2.0 PRODID:ILLC Website X-WR-TIMEZONE:Europe/Amsterdam BEGIN:VTIMEZONE TZID:Europe/Amsterdam X-LIC-LOCATION:Europe/Amsterdam BEGIN:DAYLIGHT TZOFFSETFROM:+0100 TZOFFSETTO:+0200 TZNAME:CEST DTSTART:19700329T020000 RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET DTSTART:19701025T030000 RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU END:STANDARD END:VTIMEZONE BEGIN:VEVENT UID:/NewsandEvents/Archives/2021/newsitem/12691/21 -July-2021-The-Seventh-International-Workshop-on-P roof-eXchange-for-Theorem-Proving-PxTP-2021-Virtua l DTSTAMP:20210417T191616 SUMMARY:The Seventh International Workshop on Proo f eXchange for Theorem Proving (PxTP 2021), Virtua l DTSTART;VALUE=DATE:20210721 DTEND;VALUE=DATE:20210721 LOCATION:Virtual DESCRIPTION:The progress in computer-aided reasoni ng, both automatic and interactive, during the pas t decades, has made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle lar ger problems progressively faster. In recent years , cooperation of such tools in larger verification environments has demonstrated the potential to re duce the amount of manual intervention. Examples i nclude the Sledgehammer tool providing an interfac e between Isabelle and (untrusted) automated prove rs, and collaboration of the HOL Light and Isabell e systems in the formal proof of the Kepler conjec ture. Cooperation between reasoning systems relie s on availability of theoretical formalisms and pr actical tools for exchanging problems, proofs, and models. The PxTP workshop strives to encourage su ch cooperation by inviting contributions on suitab le integration, translation, and communication met hods, standards, protocols, and programming interf aces. The workshop welcomes developers of automate d and interactive theorem proving tools, developer s of combined systems, developers and users of tra nslation tools and interfaces, and producers of st andards and protocols. We are interested both in s uccess stories and descriptions of current bottlen ecks and proposals for improvement. Topics of int erest for this workshop include all aspects of coo peration between reasoning tools, whether automati c or interactive. Researchers interested in partic ipating are invited to submit either an extended a bstract (up to 8 pages) or a regular paper (up to 15 pages). Submitted papers should describe previo usly unpublished work, and must be prepared using the LaTeX EPTCS class. Submissions will be referee d by the program committee, which will select a ba lanced program of high-quality contributions. Shor t submissions that could stimulate fruitful discus sion at the workshop are particularly welcome. We expect that one author of every accepted paper wil l present their work at the workshop. X-ALT-DESC;FMTTYPE=text/html:
\n

The progr ess in computer-aided reasoning, both automatic an d interactive, during the past decades, has made i t possible to build deduction tools that are incre asingly more applicable to a wider range of proble ms and are able to tackle larger problems progress ively faster. In recent years, cooperation of such tools in larger verification environments has dem onstrated the potential to reduce the amount of ma nual intervention. Examples include the Sledgehamm er tool providing an interface between Isabelle an d (untrusted) automated provers, and collaboration of the HOL Light and Isabelle systems in the form al proof of the Kepler conjecture.

\n\n

Coo peration between reasoning systems relies on avail ability of theoretical formalisms and practical to ols for exchanging problems, proofs, and models. T he PxTP workshop strives to encourage such coopera tion by inviting contributions on suitable integra tion, translation, and communication methods, stan dards, protocols, and programming interfaces. The workshop welcomes developers of automated and inte ractive theorem proving tools, developers of combi ned systems, developers and users of translation t ools and interfaces, and producers of standards an d protocols. We are interested both in success sto ries and descriptions of current bottlenecks and p roposals for improvement.

\n
\n

T opics of interest for this workshop include all as pects of cooperation between reasoning tools, whet her automatic or interactive. Researchers interest ed in participating are invited to submit either a n extended abstract (up to 8 pages) or a regular p aper (up to 15 pages). Submitted papers should des cribe previously unpublished work, and must be pre pared using the LaTeX EPTCS class. Submissions wil l be refereed by the program committee, which will select a balanced program of high-quality contrib utions. Short submissions that could stimulate fru itful discussion at the workshop are particularly welcome. We expect that one author of every accept ed paper will present their work at the workshop.< /p>\n

URL:https://pxtp.gitlab.io/2021 END:VEVENT END:VCALENDAR