[Hol-info] International Workshop on Quantification (QUANTIFY 2024)
Call for Contributions International Workshop on Quantification (QUANTIFY 2024) (co-located with the International Joint Conference on Automated Reasoning, IJCAR 2024) https://qbf24.pages.sai.jku.at/quantify/ *** Important Dates *** (Extended) === * Round 1 (notification before early registration deadline) Submission: May 15 for paper categories, May 25 for talk abstracts, Notification: May 30 * Round 2 (notification after early registration deadline) Submission: June 10 (talk abstracts only!) Notification: June 15 * Workshop: July 1 *** Overview *** Quantifiers play an important role in language extensions of many logics. The use of quantifiers often allows for a more succinct encoding as it would be possible without quantifiers. However, the introduction of quantifiers affects the complexity of the extended formalism in general. In consequence, theoretical results established for the quantifier-free formalism may not directly be transferred to the quantified case. Further, techniques successfully implemented in reasoning tools for quantifier-free formulas cannot directly be lifted to a quantified version. The goal of the Workshop on Quantification (QUANTIFY 2024) is to bring together researchers who investigate the impact of quantification from a theoretical as well as from a practical point of view. Quantification is a topic in different research areas, e.g., in SAT in terms of QBF, in CSP in terms of QCSP, in SMT, ATP, Computer Algebra, etc. This workshop has the aim to provide an interdisciplinary forum where researchers of various fields may exchange their experiences. In particular, the following topics shall be considered at the workshop: * Theoretical aspects of quantification. * Practical aspects of quantification. * Intersections between the different research communities working on quantification. *** Organizers *** * Konstantin Korovin, University of Manchester, UK * Martina Seidl, Johannes Kepler University Linz, Austria *** Program Committee *** Erika Abraham, RWTH Aachen University Hubie Chen, Kingâs College London Pascal Fontaine, Université de Liège, Belgium Alberto Griggio, Fondazione Bruno Kessler Konstantin Korovin, University of Manchester, UK (co-chair) Stephan Schulz, DHBW Stuttgart Martina Seidl, Johannes Kepler University Linz, Austria (co-chair) Friedrich Slivovsky, University of Liverpool Geoff Sutcliffe, University of Miami *** Submission *** Submissions of extended abstracts, full papers, and tutorials are solicited and will be managed via Easychair: https://easychair.org/conferences/?conf=quantify24 Submitted papers should be formatted in LNCS format. We solicit three types of submissions: * Talk abstracts (maximum two pages, excluding references) describing already published results. * Full papers (maximum 15 pages, excluding references) on novel, unpublished work. * Tutorial papers (maximum 15 pages, excluding references) introducing a research field related to quantifiers. The talk abstracts should include a relevant bibliography of related work and an outline of the planned talk. For this category, we explicitly advocate talks which summarize the results of one or more already published papers. Full papers should contain novel, unpublished work that qualifies to be published in a special issue of a journal or formal workshop proceedings. Tutorial papers shoul survey results already published, maybe in multiple articles or presentations capturing the commonalities and differences of various quantification approaches (perhaps even interdisciplinary). Each submission will be assessed by the program committee and the workshop organizers with respect to novelty, originality, and scope. Submissions related to completed work as well as work in progress are welcome. Authors are encouraged to provide additional material such as source code of tools, experimental data, benchmarks and related publications in an appendix or a related webpage. The additional material will be considered at the discretion of the reviewers. Previously published work or extensions thereof may be submitted to the workshop but that case has to be explicitly stated in the submitted paper. This regulation also applies to work which is currently under review elsewhere. Authors of accepted abstracts and papers are expected to give a talk at the workshop. *** Plans for Publications *** The outcomes of the discussions will be summarized in a workshop report, which can be made publicly available as technical report (unless the participants decide not to do so). In case we get enough full and tutorial papers, we will organize a special issue on quantificaton (e.g., in the Journal of Satisfiablity (JSAT) or formal workshop proceedings. *** Contact *** For any
[Hol-info] The 18th International Conference on Reachability Problems - RP 2024
Call for Papers The 18th International Conference on Reachability Problems - RP 2024 September 25-27, 2024, TU Wien, Vienna, Austria https://easychair.org/smart-program/RP24/index.html **Overview** The 18th International Conference on Reachability Problems (RP'24) is being organised as a physical meeting by the Formal Methods in Systems Engineering Research Unit of the Faculty of Informatics at the TU Wien. The conference is aimed at gathering together scholars from diverse disciplines and backgrounds interested in reachability problems that appear in - Algebraic structures - Automata theory and formal languages - Computational game theory - Concurrency and distributed computation - Decision procedures in computational models - Hybrid dynamical systems - Logic and model checking - Verification of finite and infinite-state systems **Program Chairs and Committee** The program committee is available at https://easychair.org/smart-program/RP24/PC.html and co-chaired by - Laura Kovacs, TU Wien - Ana Sokolova, U. Salzburg **Submission categories** Original research papers (up to 12 pages) and presentation-only contributions (short abstract), with clear relevance to reachability problems, are both encouraged. Topics of interest include (but are not limited to): - reachability problems in infinite-state systems - rewriting systems - dynamical and hybrid systems - reachability problems in logic and verification - reachability analysis in different computational models - counter timed/ cellular/ communicating automata - Petri nets - computational and combinatorial aspects of algebraic structures (semigroups, groups and rings) - frontiers between decidable and undecidable reachability problems predictability in iterative maps and new computational paradigms. **Submission instructions** Submissions should be prepared using the Springer LNCS guidelines and submitted via the link https://easychair.org/conferences/?conf=rp24 Accepted original papers will be published in the Springer LNCS proceedings of RP'24. **Important dates** Original Full Papers (12 pages) - Abstracts of original full papers: May 27, 2024 - Original full papers: May 30, 2024 - Full paper notifications: July 11, 2024 - Final version: July 22, 2024 Presentation-Only Contributions (4 pages) - Abstracts of presentation-only contributions: July, 27, 2024 - Presentation-only notifications: August 8, 2024 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] PAAR 2024 - Call for Papers - Extended Deadlines
** PAAR-2024: 9TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING -- co-located with IJCAR 2024 -- July 2, 2024, Nancy, France Web site: https://paar2024.github.io/ Submission link: https://easychair.org/conferences/?conf=paar2024 Abstract registration deadline (extended): April 19, 2024 Submission deadline (extended) : April 26, 2024 Topics: automated reasoning, implementation, tools ** The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well-behaved in practice, and connect well to application domains? which reasoning tasks are tractable and useful? which algorithms are able to solve real-world instances? how should automated reasoning tools be designed, implemented, tested, and evaluated? The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies. Submission Guidelines - Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages), excluding references, via EasyChair at https://easychair.org/conferences/?conf=paar2024. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. Submissions should be prepared in LaTeX using the CEUR-WS.org style template (CEURART, one-column). The package containing the class file and the user guide can be downloaded from http://ceur-ws.org/Vol-XXX/CEURART.zip. Topics include, but are not limited to: -- * automated reasoning in propositional, first-order, higher-order, and non-classical logics; * implementation of provers (SAT, SMT, resolution, superposition, tableau, instantiation-based, rewriting, logical frameworks, etc.); * automated reasoning tools for all kinds of practical problems and applications; * pragmatics of automated reasoning within proof assistants; * practical experiences, usability aspects, feasibility studies; * evaluation of implementation techniques and automated reasoning tools; * performance aspects, benchmarking approaches; non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications; * implementation techniques, optimisation techniques, machine learning, strategies and heuristics, fairness; * tools or methods that support prover development; * system descriptions and demos. Invited Speakers --- * N.N. * N.N. Programme Committee --- * Claudia Nalon, University of Brasilia, BR (PC co-chair) * Alexander Steen, University of Greifswald, DE (PC co-chair) * Martin Suda, Czech Technical University in Prague, CZ (PC co-chair) * Gabriel Ebner, Microsoft Research, US * Mathias Fleury, University of Freiburg, DE * Pascal Fontaine, Universite de Liege, BE * Ulrich Furbach, University of Koblenz, DE * Jan Jakubuv, Czech Technical University in Prague, CZ * Cezary Kaliszyk, University of Innsbruck, AT * Daniela Kaufmann, TU Vienna, AU * Boris Konev, University of Liverpool, UK * Daniel Le Berre, CNRS - Universite d'Artois, FR * Ondrej Lengal, Brno University of Technology, CZ * Tomer Libal, University of Luxembourg, LU * Hans de Nivelle, Nazarbayev University, KZ * Michael Rawson, TU Vienna, AU * Philipp Ruemmer, Uppsala University, SE * Renate A. Schmidt, The University of Manchester, UK * Stephan Schulz, DHBW Stuttgart, DE * Frieder Stolzenburg, Harz University of Applied Sciences, DE * Geoff Sutcliffe, University of Miami, US * Sophie Tourret, Inria and MPI for Informatics, DE * Zsolt Zombori, Alfred Renyi Institute of Mathematics, Hungarian Academy of Sciences, HU Publication --- PAAR proceedings will be published electronically in a workshop proceedings venue (such as CEUR workshop proceedings or EasyChair Kalpa proceedings). Venue
[Hol-info] iFM 2024 Call for Papers
iFM 2024 Call for Papers - 19th International Conference on Integrated Formal Methods https://ifm2024.cs.manchester.ac.uk/ ***Objectives and scope*** In the last decades, we have witnessed a proliferation of approaches that integrate several modelling, verification and simulation techniques, facilitating more versatile and efficient analysis of software-intensive systems. These approaches provide powerful support for the analysis of different functional and non-functional properties of the systems, complex interaction of components of different nature as well as validation of diverse aspects of system behaviour. The iFM conference series is a forum for discussing recent research advances in the development of integrated approaches to formal modelling and analysis. The conference covers all aspects of the design of integrated techniques, including language design, verification and validation, automated tool support and the use of such techniques in software engineering practice. To credit the effort of tool developers, we use EAPLS artifact badging. Areas of interest include (but are not limited to): - Formal and semi-formal modelling notations - Combining formal methods with different performance, simulation and system analysis techniques - Program verification, model checking, and static analysis - Theorem proving, decision procedures and SAT/SMT solving - Runtime analysis, monitoring and testing - Program synthesis - Modelling, analysis and synthesis of cyber-physical, hybrid, embedded, probabilistic, distributed or concurrent systems - Abstraction and refinement - Model learning and inference - Approaches to integrating formal methods into software engineering practice or industry - Approaches to integrating formal methods into standardisation or certification processes - Formal methods for artificial intelligence, including machine learning and data-based techniques - Tools and case studies supporting the integration of formal methods ***Important Dates (AoE)*** Abstract submission: 3 June 2024 Paper submission: 10 June 2024 Acceptance notification: 5 August 2024 Artifact Registration: 12 August 2024 Artifact Submission: 19 August 2024 Artifact Notification: 16 September 2024 Camera-ready: 18 September 2024 iFM 2024 main conference: 13-15 November 2024 ***Paper Categories*** iFM 2024 solicits high-quality papers reporting research results and/or experience reports related to the overall theme of formal methods integration. We solicit papers in the following categories: (1) Regular papers (limit 16 pages) presenting original scientific research results, tools, their foundation and evaluations, applications of formal methods, including rigorous evaluations and case studies. (2) Short papers (limit 6 pages) describing any work in the area of formal methods, including work-in-progress and preliminary results that are sufficiently interesting for the iFM community. All page limits exclude the references. Appendices may be included, but they will only be read by a reviewer at their discretion. Regular and short papers must be original, unpublished, and not submitted for publication elsewhere. Papers will undergo a thorough review process. Submissions will be judged on the basis of significance, relevance, correctness, originality, and clarity. The submissions will be reviewed and selected for publication based on the above-mentioned criteria as well as suitability to the conferenceâs technical program. The review process is single blind. ***Submission guidelines*** Submissions for all categories should be made using the iFM 2024 EasyChair site: https://easychair.org/conferences/?conf=ifm24 Submissions must be in PDF format, using the Springer LNCS style files. Springer requires that authors should consult Springerâs authorsâ guidelines and use their proceedings templates, either for LaTeX or for Word, for the preparation of their papers. Springer encourages authors to include their ORCIDs in their papers. After a paper is accepted, the corresponding author of each paper, acting on behalf of all of the authors of that paper, must complete and sign a Consent-to-Publish form. The corresponding author signing the copyright form should match the corresponding author marked on the paper. Once the files have been sent to Springer, changes relating to the authorship of the papers cannot be made. The conference proceedings will be published in Springerâs Lecture Notes in Computer Science series. A special issue of the Formal Aspects of Computing journal is planned for extended versions of selected papers from iFM 2024. All accepted papers must be presented at the conference. At least one author of each accepted paper must register to the conference by the early registration date. ***EAPLS Artifact Badging*** Reproducibility of experiments is crucial to foster an atmosphere of open, reusable and trustworthy research. To improve and reward
[Hol-info] LPAR 2024 short presentation papers - CFP
** The 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-25 Mauritius, 26-31st May 2024 https://lpar-25.info CALL FOR SHORT PRESENTATION PAPERS In keeping with the tradition of LPAR, researchers and practitioners are invited to submit short presentation papers (the papers can be full length, the presentation slots will be short), reporting on interesting work in progress, system and tool descriptions, experimental results, etc. They need not be original, and extended or revised versions of the papers may be submitted concurrently with or after LPAR to another conference or a journal. Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will not be published. The short presentation papers will be published electronically as a volume in the Kalpa series, see http://www.easychair.org/publications/Kalpa. The LaTeX and Microsoft Word templates for the Kalpa series can be downloaded from http://www.easychair.org/publications/for_authors. Papers may be up to 15 pages long, and must be submitted through the EasyChair system using the web page https://easychair.org/conferences/?conf=lpar2024. Paper submission deadline: 15th April 2024 Notification of acceptance: 22nd April 2024 Final version: 16th May 2024 ... however, in order to facilitate authors making travel arrangements, papers submitted before the deadline will be reviewed immediately, and a decision made in approximately 2-3 days. Submit early, submit boldly, and submit often! ** ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CICM 2024 - Extended deadline - Call for Papers
Call for Papers - formal papers - doctoral programme 17th Conference on Intelligent Computer Mathematics - CICM 2024 - August 5â9, 2024 Montréal, Canada https://cicm-conference.org/2024/ More and more mathematical information is digitally processed, generated, communicated, stored and curated. CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration. CICM 2024 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to * theorem proving and computer algebra * mathematical knowledge management * digital mathematical libraries *** Important Dates *** Formal submissions - Abstract deadline: April 1, 2024 (extended) - Full paper deadline:April 8, 2024 (extended) - Reviews sent to authors:May 14, 2024 (extended) - Rebuttals: May 14-17, 2024 (extended) - Notification of acceptance: May 28, 2024 (extended) - Camera-ready copies due:June 11, 2024 (extended) - Conference: August 5-9, 2024 Doctoral programme applications - Submission deadline: June 13, 2024 - Notification of acceptance:June 28, 2024 *** Programme committee *** The program committee is listed at https://cicm-conference.org/2024/cicm.php?event==pc The program committee is chaired by Andrea Kohlhase (Neu-Ulm University of Applied Sciences, Germany) and Laura Kovács (TU Vienna, Austria). The CICM community appreciates the varying nature of the relevant research in computer mathematics and invites submissions of two different forms: *** Formal Paper Submissions *** Formal submissions will be reviewed rigorously and accepted papers will be published in a volume of Springer LNAI: * regular papers (up to 15 pages + bibliography) present novel research results * project and survey papers (up to 15 pages + bibliography) summarize existing results * system and dataset descriptions (4 to 5 pages + bibliography) present digital artifacts *** Doctoral Symposium: Two-Page Abstracts*** The doctoral programme provides PhD students a forum to present early results to receive constructive feedback and mentoring. To attend, submissions of two-page abstracts are expected in which the focus and research questions of the expected PhD theses are described; details on completed research tasks and remaining research plans should be given. In addition to these abstract, a two-pages CV of the applicant should also be submitted, detailing background information (name, university, supervisor), education (sought degree, previous degrees), employments and relevant research experience (publications, attended conferences/workshops). *** Submissions *** All submissions should be made via EasyChair at https://easychair.org/conferences/?conf=cicm24 using the Springer LNCS style files (see https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines). CICM 2024 proceedings, containing the accepted formal submissions, will be published in the Springer LNAI series. *** Participation - Physical Event *** CICM 2024 will be held as a physical event and participation is possible only on-site. At least one of the authors of accepted papers is expected to register to CICM 2024 and present the work(s) on-site. *** Best Papers *** CICM 2024 honors the best paper and best student paper with respect to reviews and program committee discussions with an award. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2024 Workshops
IJCAR 2024 --- Co-Located workshops. More information below. PAAR-2024: 9TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING https://paar2024.github.io/ QUANTIFY 2024: International Workshop on Quantification https://qbf24.pages.sai.jku.at/quantify/ SC-Square 2024: 9th International Workshop on Satisfiability Checking and Symbolic Computation http://www.sc-square.org/CSA/workshop9.html Termination and Complexity Competition 2024 http://www.termination-portal.org/wiki/Termination_Competition_2024 ThEdu'24: Theorem proving components for Educational software http://www.uc.pt/en/congressos/thedu/ThEdu24 UNIF 2024: The 38th International Workshop on Unification https://lat.inf.tu-dresden.de/unif2024 5th International Workshop on Automated (Co)inductive Theorem Proving https://wait2024.github.io/ The TPTP Tea Party https://www.tptp.org/TPTP/TPTPTParty/2024/ ** PAAR-2024: 9TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING -- co-located with IJCAR 2024 -- July 2, 2024, Nancy, France Web site: https://paar2024.github.io/ Submission link: https://easychair.org/conferences/?conf=paar2024 Abstract registration deadline: April 5, 2024 Submission deadline: April 12, 2024 Topics: automated reasoning, implementation, tools ** The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well-behaved in practice, and connect well to application domains? which reasoning tasks are tractable and useful? which algorithms are able to solve real-world instances? how should automated reasoning tools be designed, implemented, tested, and evaluated? The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies. Submission Guidelines - Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages), excluding references, via EasyChair at https://easychair.org/conferences/?conf=paar2024. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. Submissions should be prepared in LaTeX using the CEUR-WS.org style template (CEURART, one-column). The package containing the class file and the user guide can be downloaded from http://ceur-ws.org/Vol-XXX/CEURART.zip. Topics include, but are not limited to: -- * automated reasoning in propositional, first-order, higher-order, and non-classical logics; * implementation of provers (SAT, SMT, resolution, superposition, tableau, instantiation-based, rewriting, logical frameworks, etc.); * automated reasoning tools for all kinds of practical problems and applications; * pragmatics of automated reasoning within proof assistants; * practical experiences, usability aspects, feasibility studies; * evaluation of implementation techniques and automated reasoning tools; * performance aspects, benchmarking approaches; non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications; * implementation techniques, optimisation techniques, machine learning, strategies and heuristics, fairness; * tools or methods that support prover development; * system descriptions and demos. Invited Speakers --- * N.N. * N.N. Programme Committee --- * Cláudia Nalon, University of BrasÃlia, BR (PC co-chair) * Alexander Steen, University of Greifswald, DE (PC co-chair) * Martin Suda, Czech Technical University in Prague, CZ (PC co-chair) * to be completed Publication --- PAAR proceedings will be published electronically in a workshop proceedings venue (such as CEUR workshop proceedings or EasyChair Kalpa proceedings). Venue - IJCAR 2024 in Nancy, France Important dates --- * Abstract
[Hol-info] International Logic Olympiad
INTERNATIONAL LOGIC OLYMPIAD We are pleased to announce the International Logic Olympiad 2024 (ILO2024) â a world-wide contest on Logic for high school students. Register & learn more at https://www.logicolympiad.org/ Brief Overview: http://intrologic.stanford.edu/olympiad/introduction.php Please share this opportunity within your network; and be sure to reach out to us with any feedback and/or willingness to contribute to this initiative. Key Benefits For Students: * Academic Achievements: Cash prizes and academic certificates * Cultural Exchange: Global learning experiences and international community * Mentorship Opportunities: Guidance from experts in logic and related fields * Exclusive opportunities for Finalists: Invitation to the Stanford University campus Key Benefits For For schools: * Global Recognition: Reputation with international acclaim * Networking Opportunities: Connection to top universities * Collaborative Projects: Cross-border collaborations and initiatives Important Deadlines: Feb 12: Open registration begins April-May: 3 Preliminary rounds July 1-3: Final Round at Stanford ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-25, Call for Short Presentation Papers
** The 25th International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-25 Mauritius, 26-31st May 2024 https://lpar-25.info CALL FOR SHORT PRESENTATION PAPERS In keeping with the tradition of LPAR, researchers and practitioners are invited to submit short presentation papers (the papers can be full length, the presentation slots will be short), reporting on interesting work in progress, system and tool descriptions, experimental results, etc. They need not be original, and extended or revised versions of the papers may be submitted concurrently with or after LPAR to another conference or a journal. Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will not be published. The short presentation papers will be published electronically as a volume in the Kalpa series, see http://www.easychair.org/publications/Kalpa. The LaTeX and Microsoft Word templates for the Kalpa series can be downloaded from http://www.easychair.org/publications/for_authors. Papers may be up to 15 pages long, and must be submitted through the EasyChair system using the web page https://easychair.org/conferences/?conf=lpar2024. Paper submission deadline: 15th April 2024 Notification of acceptance: 17st April 2024 Final version: 22th April 2024 ... however, in order to facilitate authors making travel arrangements, papers submitted before the deadline will be reviewed immediately, and a decision made in approximately 2-3 days. Submit early, submit boldly, and submit often! ** ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Bill McCune PhD Award in Automated Reasoning 2024 Call for Nominations
The Bill McCune PhD Award in Automated Reasoning 2024 Call for Nominations http://cadeinc.org/McCune-Award *** Automated Reasoning is the area of Computer Science dedicated to applying reasoning in the form of logic to computing systems. The Bill McCune PhD Award in Automated Reasoning distinguishes each year a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. The award is named after the American computer scientist William Walker McCune, known for his contributions in the fields of Automated Reasoning, Algebra, Logic, and Formal Methods. He was the implementer of OTTER, Prover9 and Mace 4, automated tools for first-order reasoning which are known to this day for their accuracy and robustness. He was also known for his generosity towards research colleagues and as a great supporter of young researchers in the field. * Eligibility * Eligible for the award are those who successfully defended their PhD - at an academic institution; - in the field of Automated Reasoning; and - in the period from 1 January 2023 - 31 December 2023. The PhD students supervised or co-supervised by the Expert Committee members are not eligible. * Nomination * Candidates for the award must be nominated by their supervisor(s) and one additional independent researcher who reviewed/examined the thesis. Nominations are to be submitted via email sent to c.f...@bbk.ac.uk, by 5 April 2024 (Anywhere on Earth). The nomination must consist of one compressed file (.zip) containing: - a letter from the supervisor(s) describing why the thesis should be considered for the award and the relationship of the contributions to CADE/IJCAR; - a report from the nominating additional independent researcher who reviewed/examined the thesis; - the thesis itself; - a copy of the PhD diploma; and - a copy of relevant papers by the nominee, if any, containing results published in the thesis. * Procedure * The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated Reasoning. - The nominations will be evaluated and compared by an international Expert Committee (see below). - The procedure to be followed is analogous to the review phase of a conference. The justification by the supervisor and the nominating additional independent researcher report will play an important role in the evaluation. - The final decision is made by the Expert Committee at least one month before CADE/IJCAR is being held. - The award consists of a certificate announcing the winner to have received the Bill McCune PhD Award in Automated Reasoning. The award will be announced at the respective year's CADE/IJCAR. The nominators of the winner will also receive a copy of this certificate. The recipient of the award is expected to attend the award ceremony. - The decision of the Expert Committee is final and cannot be appealed. * Expert Committee * The Expert Committee, consisting of leading researchers in Automating Reasoning, is formed by the board of CADE Trustees with the aim to reflect the broad diversity in the area of Automated Reasoning. It is announced with the call for nominations, and thus formed before this call. The decision on the award is taken by the Expert Committee. The Expert Committee can seek additional expertise, even after the submission deadline for nominations. Expert Committee members cannot nominate a PhD student. Expert Committee members cannot contribute an independent report seconding a nomination. The Expert Committee for the Bill McCune PhD Award 2024 consists of the following people: - Haniel Barbosa, Universidade Federal de Minas Gerais - Pascal Fontaine, University of Liege - Carsten Fuhs, Birkbeck, University of London (chair) - Laura Kovacs, TU Wien - Claudia Nalon, University of Brasilia - Philipp Ruemmer, University of Regensburg - Martina Seidl, Johannes Kepler University - Viorica Sofronie-Stokkermans, University of Koblenz - Rene Thiemann, University of Innsbruck - Sophie Tourret, Inria - LORIA *** ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 2024 Alonzo Church Award Call for Nominations
CALL FOR NOMINATIONS The 2024 Alonzo Church Award for Outstanding Contributions to Logic and Computation INTRODUCTION An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Goedel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see https://siglog.org/alonzo-church-award/, https://www.eatcs.org/index.php/church-award/, and https://www.eacsl.org/alonzo-church-award/. The 2023 Alonzo Church Award was jointly to Lars Birkedal, AleÅ¡ Bizjak, Derek Dreyer, Jacques-Henri Jourdan, Ralf Jung, Robbert Krebbers, Filip Sieczkowski, Kasper Svendsen, David Swasey and Aaron Turon for the design and implementation of Iris, a higher-order concurrent separation logic framework. ELIGIBILITY AND NOMINATIONS The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2024 award, the cut-off date is January 1, 1999. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Goedel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference. Nominations for the 2024 award are now being solicited. The nominating letter must summarise the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness. Nominations for the 2024 award are automatically considered for all future editions of the award, until they receive the award or the nominated papers are no longer eligible. Nominations should be submitted to igor.walukiew...@gmail.com by March 1, 2024. PRESENTATION OF THE AWARD The 2024 award will be presented at the Thirty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) which is scheduled to take place in Tallinn, Estonia during 8â12 July 2024. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CICM 2024 - 17th Conference on Intelligent Computer Mathematics - Call for Papers
Call for Papers formal papers - doctoral programme 17th Conference on Intelligent Computer Mathematics - CICM 2024 - August 5-9, 2024 Montreal, Canada https://cicm-conference.org/2024/ --- More and more mathematical information is digitally processed, generated, communicated, stored and curated. CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration. CICM 2024 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to * theorem proving and computer algebra * mathematical knowledge management * digital mathematical libraries *** Important Dates *** Formal submissions - Abstract deadline: March 11, 2024 - Full paper deadline: March 18, 2024 - Reviews sent to authors:April 29, 2024 - Rebuttals due: May 1, 2024 - Notification of acceptance: May 16, 2024 - Camera-ready copies due:June 3, 2024 - Conference: August 5-9, 2024 Doctoral programme applications - Submission deadline: June 13, 2024 - Notification of acceptance: June 28, 2024 CICM appreciates the varying nature of the relevant research in this area and invites submissions of two different forms: *** Formal Paper Submissions *** Formal submissions will be reviewed rigorously and accepted papers will be published in a volume of Springer LNAI: * regular papers (up to 15 pages + bibliography) present novel research results * project and survey papers (up to 15 pages + bibliography) summarize existing results * system and dataset descriptions (4 to 5 pages + bibliography) present digital artifacts *** Doctoral Symposium: Two-Page Abstracts*** The doctoral programme provides PhD students a forum to present early results to receive constructive feedback and mentoring. To attend, submissions of two-page abstracts are expected in which the focus and research questions of the expected PhD theses are described; details on completed research tasks and remaining research plans should be given. In addition to these abstracts, a two-page CV of the applicant should also be submitted, detailing background information (name, university, supervisor), education (sought degree, previous degrees), employments and relevant research experience (publications, attended conferences/workshops). *** Submissions *** All submissions should be made via EasyChair at https://easychair.org/conferences/?conf=3Dcicm2024 using the Springer LNCS style files https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines CICM 2024 proceedings, containing the accepted formal submissions, will be published in the Springer LNAI series. *** Participation - Physical Event *** CICM 2024 will be held as a physical event and participation is possible only on-site. At least one of the authors of accepted papers is expected to register to CICM 2024 and present the work(s) on-site. *** Best Papers *** CICM 2024 honors the best paper and best student paper with respect to reviews and program committee discussions with an award. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2024 - Call for Papers
IJCAR 2024 [Apologies if you receive multiple copies] === CALL FOR PAPERS IJCAR 2024 The 12th International Joint Conference on Automated Reasoning Nancy, France, July 1-6, 2024 https://ijcar2024.loria.fr/ === IJCAR is the premier international joint conference on all topics in automated reasoning. IJCAR 2024 will be hosted by the Inria Nancy Research Center and LORIA in Nancy, France, from July 1-6, 2024. IJCAR 2024 is the merger of leading events in automated reasoning: * CADE (Conference on Automated Deduction) * FroCoS (Symposium on Frontiers of Combining Systems) * TABLEAUX (Conference on Analytic Tableaux and Related Methods) TOPICS == IJCAR 2024 invites submissions related to all aspects of automated or interactive logical reasoning, including foundations, implementations, and applications. Original research papers and descriptions/evaluations of working automated deduction systems or proof assistant systems are solicited. IJCAR topics include the following: * Logics of interest include: propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many- valued, substructural, description, type theory. * Methods of interest include: tableaux, sequent calculi, resolution, model- elimination, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, automated theorem proving, combination of decision or proof procedures, SAT and SMT solving, machine learning and theorem proving, integration of automated provers/proof assistants in automated test generators, program synthesisers, verified compilers, intelligent systems, agent based systems, knowledge processing systems, formal methods tools and other symbolic tools, etc. * Applications of interest include: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation and processing/engineering, education, formalization of mathematics, trusted AI, etc. IMPORTANT DATES (partly tentative) 15 Jan 2024 Abstract submission deadline 22 Jan 2024 Paper submission deadline 15 Mar 2024 Notification of paper decisions (tentative) 04 Apr 2024 Camera-ready papers due (tentative) 1-2 Jul 2024 Workshops & Tutorials 3-6 Jul 2024 Conference, including CASC WORKSHOPS, TUTORIALS, SYSTEM COMPETITION == A two-day workshop and tutorial programme will be co-organized with the conference. In addition, the annual CADE ATP System Competition (CASC) will be held during the conference. Details will be published in separate calls and on the conference website. SUBMISSION GUIDELINES == IJCAR 2024 invites submissions related to the topics of interest mentioned above. All papers must be original and not simultaneously submitted to another peer-reviewed journal or conference. The following paper categories are welcome: * Regular papers describing solid new research results. They can be up to 15 pages in LNCS style, including figures but excluding references and appendices. Where applicable, regular papers are supported by experimental validation. Submissions reporting on case studies in an industrial context are strongly invited as regular papers. * Short papers describing implemented systems, user experiences, case studies and domain models, etc. They can be up to 7 pages in LNCS style, excluding references and appendices. All submissions will be judged on relevance, originality, significance, correctness, and readability. Proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, e.g., via a reference to a website or in an appendix of the paper. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chairs may solicit further reviews after the rebuttal period. All submissions must be formatted using the Springer LNCS styles and submitted in PDF via EasyChair: https://easychair.org/conferences/?conf=ijcar2024 The IJCAR 2024 proceedings will be published in the Springer series Lecture Notes in Artificial Intelligence (LNAI/LNCS) as Gold Open Access, and will be available online during the conference. All accepted papers must have one registration including the processing fees of the Gold Open Access (200 Euros per paper is foreseen, like for the previous edition of IJCAR). Authors of accepted papers are required to
[Hol-info] CFP extended - Special Issue on Non-Classical Reasoning for Contemporary AI Applications
Call for Papers Journal "KI - Künstliche Intelligenz" (German AI journal) Special Issue on Non-Classical Reasoning for Contemporary AI Applications (guest editors: C. Benzmüller and A. Steen) https://www.springer.com/journal/13218 Extended submission deadline: December 18, 2023. This special issue aims at providing an overview of recent work in automation of expressive non-classical logics, AI-related applications thereof, and discussions of perspectives in explicit symbolic knowledge representation and reasoning in contemporary AI applications regarding, but not limited to, the following topics: - Knowledge representation in non-classical logics - Automated and interactive theorem proving in non-classical logics - Applications of non-classical logics and logic automation in AI - Applications of automated reasoning in other sciences - System development and implementation techniques - Current and upcoming developments in non-classical automated reasoning Technical contributions (of up to 20 pages), abstracts (4 pages), e.g., on doctoral theses or habilitations, system descriptions (4-6 pages), project reports (4-6 pages), or discussion articles (4-8 pages), are welcome. All submissions will be peer-reviewed. The full CfP can be found at https://www.springer.com/journal/13218/updates/25263164 (but please ignore the old deadline). If you have any questions, please do not hesitate to contact me (alexander.st...@uni-greifswald.de). ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] TPTP v8.2.0 released
The TPTP Problem Library, Release v8.2.0 Geoff Sutcliffe ge...@tptp.org The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect the capabilities of the ATP system being considered. TPTP v8.2.0 is now available at: http://www.tptp.org The TPTP-v8.2.0.tgz file contains the library, including utilities and basic documentation. Full documentation is online at: http://www.tptp.org/TPTP/TR/TPTPTR.shtml == What's New in TPTP v8.2.0 == Changes from v8.1.2 to v8.2.0 for THF problems 2823 ratings changed Changes from v8.1.2 to v8.2.0 for TFF problems 9 new abstract problems 218 new problems 1013 ratings changed Changes from v8.1.2 to v8.2.0 for FOF problems 4370 ratings changed Changes from v8.1.2 to v8.2.0 for CNF problems 4158 ratings changed + In SyntaxBNF: - Separated into and . - defined as , and similarly defined as . - Removed nhf_connective and , added as a unary connective. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CADE-29 CALL FOR PARTICIPATION
== CADE-29 CALL FOR PARTICIPATION == The 29th International Conference on Automated Deduction Rome, Italy 1 July - 6 July 2023 https://easyconferences.eu/cade2023/ CADE-29 is co-located with the 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) *** KEYNOTE SPEAKERS *** Maribel Fernandez (Kings College London) (joint invited with FSCD 2023) Jasmin Blanchette (Ludwig-Maximilan Universität München) *** RESEARCH PROGRAM *** https://easyconferences.eu/cade2023/ *** WORKSHOPS *** ADeMaL: Automated Deduction for Machine Learning â Date: 05 July Vampire 2023: The 7th Vampire Workshop â Date: 05 July Theorem Proving Components for Educational Software (ThEdu'23) â Date: 05 July SMT'23: The 21st International Workshop on Satisfiability Modulo Theories â Date: 05-06 July *** SYSTEM COMPETITION *** CASC (CADE System Competition) https://www.tptp.org/CASC/29/ *** REGISTRATION *** Early registration until 31 May 2023 Late registration from 1 June 2023 *** VENUE *** The Faculty of Civil and Industrial Engineering Sapienza University of Rome *** CADE-29 ORGANIZERS *** Conference Chairs: Daniele Gorla (Sapienza University of Rome) Program Committee Chairs: Brigitte Pientka (McGill University) Cesare Tinelli (University of Iowa) Workshop & Tutorial Chair: Ivano Salvo (Sapienza University of Rome) Publicity Chair: Haniel Barbosa (Universidade Federal de Minas Gerais) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-24 in 2023, Manizales Colombia, Registration is Open
LPAR-24 in 2023: The 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning https://easychair.org/smart-program/LPAR2023/ REGISTRATION is now OPEN! The International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is an academic conference aiming at discussing cutting- edge results in the fields of automated reasoning, computational logic, programming languages and their applications. LPAR is an "A" ranked conference in the CORE ranking system; papers from previous proceedings are listed in DBLP. LPAR's slogan is "To boldly go where no reasonable conference has gone before". LPAR brings first class research and researchers to interesting places, and exposes the conference attendees to interesting cultures. The 24th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-24) will be held in Manizales, Colombia, at the Campus La Nubia of the National University of Colombia, 4-9th June 2023 (so, LPAR-24 will be in 2023 - don't get confused). ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FroCoS 2023 deadline extension
Dear colleagues, As requested by some of you, we have extended the deadline for paper submission from Monday next week (May 15) to Friday next week (May 19) - and then also the submission for title and abstracts to next Monday (May 15). The new dates are Important Dates - Submission of title and abstract: May 15, 2023 Paper submission deadline:May 19, 2023 Notification of acceptance: July 3, 2023 Final version: July 21, 2023 Conference date: September 20-22, 2023 Below is the rest of the call for papers: looking forward to your submissions, cheers, Martin Suda and Uli Sattler CALL FOR PAPERS: FroCoS 2023 === The 14th International Symposium on Frontiers of Combining Systems FroCoS 2023 will be held at the Czech Technical University in Prague in September, 2023. FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. The first FroCoS symposium was held in Munich, Germany, in 1996. Initially held every two years, since 2004 it has been organized annually with alternate years forming part of IJCAR. FroCoS 2023 will be co-located with the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023). Conference website: https://frocos2023.github.io Submission link: https://easychair.org/conferences/?conf=frocos2023 Workshops and Tutorials - If you would like to organise a workshop or run a tutorial, please let us know before July 14th, 2023. --- Submission Guidelines --- Scope The program committee seeks high-quality submissions describing original work, written in English, not overlapping with published or simultaneously submitted work to a journal or conference, workshop, symposium, etc. with archival proceedings. Selection criteria include originality of ideas, rigour of evaluation, significance of results, and quality of presentation. The page limit in Springer LNCS style is 15 pages in total excluding references. Papers must be edited in LaTeX using the LLNCS style and must be submitted electronically as PDF files via EasyChair at https://easychair.org/conferences/?conf=frocos2023 For each accepted paper, at least one of the authors is required to register to the symposium and present the work. Formatting instructions and the LLNCS style files can be obtained at http://www.springer.com/br/computer-science/lncs/conference-proceedings-guidelin es The FroCoS 2023 conference proceedings will be published in the Springer series Lecture Notes in Artificial Intelligence (LNAI/LNCS) as Gold Open Access under a CC-BY-4.0-license, for a cost of max. 200 Euros per paper, with at least 5 full sponsorships available for authors lacking funds. Details on how to apply for sponsorship will be announced soon. List of Topics -- Topics of interest for FroCoS 2023 include (but are not restricted to): Combinations of - logics such as higher-order, first-order, temporal, modal, description or other non-classical logics - logics with probability and/or fuzzy measures - reasoning procedures, SAT solvers, constraint solving techniques, logical frameworks, deduction methods, and constraint propagation - logics for distributed and multi-agent systems - term rewriting systems - logical reasoning with machine learning - logics, reasoning, and natural language processing/semantics - programs and specifications and their logical aspects, incl. modularisation Integration of - equational and other theories into deductive systems, incl. SMT - data structures into constraint logic programming and deduction Modularity - of/in logics - in term rewriting and the application of any of these, for example for knowledge representation, ontology engineering, and the verification or analysis of information systems. Invited Speakers To be announced Programme Committee - Carlos Areces, FaMAF - Universidad Nacional de Córdoba Alessandro Artale, Free University of Bolzano-Bozen Franz Baader, TU Dresden Haniel Barbosa, Universidade Federal de Minas Gerais Peter Baumgartner, CSIRO Clare Dixon, University of Manchester Mathias Fleury, University of Freiburg Didier Galmiche, LORIA - Université de Lorraine Silvio Ghilardi, Dipartimento di Matematica, Università degli Studi di Milano Jürgen Giesl, RWTH Aachen University Andreas Herzig, IRIT at Université Paul Sabatier Jean Christoph Jung, Universität Bremen Roman Kontchakov Birkbeck, University of London Paliath Narendran, University at Albany - SUNY Aina Niemetz, Stanford University Naoki Nishida, Nagoya University Giles Reger, Amazon Web Services and The University of Manchester Andrew Reynolds, The University of Iowa Christophe Ringeissen, LORIA - Université de Lorraine Philipp Rümmer, Uppsala
[Hol-info] 14th IWIL workshop, FINAL CALL FOR PAPERS: 2nd Round Deadline May 15th AoE 2023
14th International Workshop on the Implementation of Logics https://eprover.org/EVENTS/IWIL-2023.html FINAL CALL FOR PAPERS: 2nd Round Deadline May 15th AoE 2023. == The 14th International Workshop on the Implementation of Logics will be held on June 4th, 2023, in conjunction with the 24th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, in Manizales, Colombia. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: Propositional logic and decision procedures, including SMT First-order and higher order logics Non-classical logics, including modal, temporal, description, non-monotonic reasoning Formal foundations for efficient implementation of logics Data structures and algorithms for the efficient representation and processing of logical concepts Proof/model search organization and heuristics for logical reasoning systems Data analysis and machine learning approaches to search control Techniques for proof/model search visualization and analysis Practical constraint handling Reasoning with ontologies and other large theories Implementation of efficient theorem provers and model finders for different logics System descriptions of logical reasoning systems Issues of reliability, witness generation, and witness verification Evaluation and benchmarking of provers and other logic-based systems I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15 pages) via the EasyChair page for IWIL2023: https://easychair.org/conferences/?conf=iwil2023 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. The proceedings will be published as a volume of Kalpa Publications in Computing. Important Dates: Submission of papers/abstracts: May 15th, 2023 Notification of acceptance: ASAP, 2023 Camera ready versions due: TBD, 2023 Workshop: June 4th, 2023 Program committee (so far - more coming): Konstantin Korovin (Co-Chair) University of Manchester Stephan Schulz (Co-Chair) DHBW Stuttgart Michael Rawson (Co-Chair) TU Wien Katalin Fazekas TU Wien Jasmin Blanchette Ludwig-Maximilians-Universität München Simon Schwarz Max-Planck-Institute for Informatics Franz BrauÃe University of Manchester Petra Hozzová TU Wien Johannes Schoisswohl TU Wien Alexander Steen Uni Greifswald Jan Jakubův Czech Technical University Boris Konev University of Liverpool Daniela Kaufmann TU Wien Christoph Wernhard University of Potsdam Giles Reger Amazon Web Services, University of Manchester Armin Biere University of Freiburg Yevgeny Kazakov The University of Ulm Martina Seidl Johannes Kepler University Linz Eugenia Ternovska Simon Fraser University Haniel Barbosa Universidade Federal de Minas Gerais Ahmed Bhayat University of Manchester Andrew Reynolds University of Iowa Jens Otten University of Oslo Pascal Fontaine Université de Liège, Belgium (more to follow) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-24 (June 2023) - Call for Short Papers
The 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-24 Manizales Colombia, 4-9th June 2023 https://easychair.org/smart-program/LPAR2023/ CALL FOR SHORT PRESENTATION PAPERS In keeping with the tradition of LPAR, researchers and practitioners are invited to submit short presentation papers (the papers can be full length, the presentation slots will be short), reporting on interesting work in progress, system and tool descriptions, experimental results, etc. They need not be original, and extended or revised versions of the papers may be submitted concurrently with or after LPAR to another conference or a journal. Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will not be published. The short presentation papers will be published electronically as a volume in the Kalpa series, see http://www.easychair.org/publications/Kalpa. The LaTeX and Microsoft Word templates for the Kalpa series can be downloaded from http://www.easychair.org/publications/for_authors. Papers may be up to 15 pages long, and must be submitted through the EasyChair system using the web page https://easychair.org/conferences/?conf=lpar23 Paper submission deadline: 19th May 2023 Notification of acceptance: 21st May 2023 Final version: 26th May 2023 ... however, in order to facilitate authors making travel arrangements, papers submitted before the deadline will be reviewed immediately, and a decision made in approximately 2-3 days. Submit early, and submit often! ** ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 7th Vampire workshop - Call for Papers
The 7th Vampire workshop is held as an affiliated event of CADE 2023. The workshop addresses recent trends in implementing first-order theorem provers, and focus on new challenges and application areas. The workshop also discusses the development and use of the first-order theorem prover Vampire, and its potential use cases and interaction with other systems. Workshop participants include both Vampire developers and users, with discussions between tool developers and users. Participants can learn more about the use of Vampire, its efficiency in various application areas and needs of the users. We seek submissions reporting on theory, application, case studies, experiments and work-in-progress using Vampire and other theorem provers in various applications. Submissions can be in any form, ranging from work in progress to completed work. For example, the users can submit: - extended abstracts or full papers; - theoretical papers; - experimental papers and case studies - or in general any papers that can benefit tool developers and users. Papers can be of any length, ranging from 1-page abstracts to full papers up to 20 pages in length. The papers should use the EasyChair templates, which can be found at https://easychair.org/publications/for_authors Submissions should be made using EasyChair, via the link https://easychair.org/conferences/?conf=vampire23. We will consider workshop post-proceedings in the EasyChair EPiC series. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CFP: 14th International Workshop on the Implementation of Logics
14th International Workshop on the Implementation of Logics https://eprover.org/EVENTS/IWIL-2023.html CALL FOR PAPERS: deadline April 10th, 2023. https://easychair.org/cfp/IWIL2023 The 14th International Workshop on the Implementation of Logics will be held on June 4th, 2023, in conjunction with the 24th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, in Manizales, Colombia. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: + Propositional logic and decision procedures, including SMT + First-order and higher order logics + Non-classical logics, including modal, temporal, description, non-monotonic reasoning + Formal foundations for efficient implementation of logics + Data structures and algorithms for the efficient representation and processing of logical concepts + Proof/model search organization and heuristics for logical reasoning systems + Data analysis and machine learning approaches to search control + Techniques for proof/model search visualization and analysis + Practical constraint handling + Reasoning with ontologies and other large theories + Implementation of efficient theorem provers and model finders for different logics + System descriptions of logical reasoning systems + Issues of reliability, witness generation, and witness verification + Evaluation and benchmarking of provers and other logic-based systems + I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15 pages) via the EasyChair page for IWIL2023: https://easychair.org/conferences/?conf=iwil2023 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. The proceedings will be published as a volume of Kalpa Publications in Computing. Important Dates: Submission of papers/abstracts: April 10th, 2023 Notification of acceptance: May 2nd, 2023 Camera ready versions due: May 22nd, 2023 Workshop: June 4th, 2023 Program committee (so far - more coming): Konstantin Korovin (Co-Chair) University of Manchester Stephan Schulz (Co-Chair) DHBW Stuttgart Michael Rawson (Co-Chair) TU Wien Katalin Fazekas TU Wien Jasmin Blanchette Ludwig-Maximilians-Universität München Simon Schwarz Max-Planck-Institute for Informatics Franz BrauÃe University of Manchester Petra Hozzová TU Wien Johannes Schoisswohl TU Wien Alexander Steen Uni Greifswald Jan Jakubův Czech Technical University Boris Konev University of Liverpool Daniela Kaufmann TU Wien Christoph Wernhard University of Potsdam Giles Reger Amazon Web Services, University of Manchester Armin Biere University of Freiburg Yevgeny Kazakov The University of Ulm Martina Seidl Johannes Kepler University Linz Eugenia Ternovska Simon Fraser University Haniel Barbosa Universidade Federal de Minas Gerais Ahmed Bhayat University of Manchester Andrew Reynolds University of Iowa Jens Otten University of Oslo Pascal Fontaine Université de Liège, Belgium (more to follow) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CADE-29 second Call for Papers
** SECOND CALL FOR PAPERS CADE-29: 29th international Conference on Automated Deduction Sapienza University of Rome Rome, Italy, 1-5 July 2023 https://easyconferences.eu/cade2023 ** -- Overview -- CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including logical foundations, theory and principles, applications in and beyond computer science and mathematics, and implementations of automated reasoning systems are solicited. CADE-29 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction. CADE-29 is in cooperation with ACM SIGLOG. -- Venue -- CADE-29 and affiliated satellite events will take place in Rome, Italy and will be co-located with FSCD 2023. -- Publication -- CADE-29 proceedings will be published in Springer's Lecture Notes in Artificial Intelligence series in Gold Open Access mode at a CADE special rate of â¬200.00 per paper. Funding will be available for authors of accepted papers who cannot cover the â¬200 fee. -- Special Issue -- The authors of a selection of the best CADE-29 papers will be invited to submit an extended version of their paper after the conference, to be published in a special issue of the Journal of Automated Reasoning. -- Submission Guidelines -- Submissions can be made in two categories: - **Regular papers**. Up to 15 pages in LNCS style, excluding references. Proofs of theoretical results that do not fit in the page limit may be provided in an appendix. - **Short papers**. This includes system descriptions, user experiences, case studies and domain models. Up to 10 pages in LNCS style, excluding references. Reviewers may consider material provided in appendices, but submissions must be self-contained within the page limit. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, originality, significance, correctness, and readability. If software or data is relevant to a paper, a link that provides access to the software/data must be provided to enable reproduction of results. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chairs may solicit further reviews after the rebuttal period. Selected accepted papers will be considered by Program Committee for the CADE Best Paper Award. Papers must be submitted to https://easychair.org/conferences/?conf=cade29 All submission must be formatted in the LNCS style and must include the ORCID id of at least the corresponding author, and preferably of all authors. -- Important Dates -- Abstract deadline: February 27, 2023 Submission deadline:March 6, 2023 Rebuttal phase: April 18-20, 2023 Notification: May 3, 2023 Final version: May 24, 2023 Main Conference:July 1-4, 2023 Satellite events: July 4-5, 2023 -- Program Committee Chairs -- Brigitte Pientka, MacGill University Cesare Tinelli, The University of Iowa -- Policies-- CADE implements the ACM policy against harassment. -- Contacts -- All questions about CADE-29 paper submissions should be emailed to the PC Chairs (cade29 at easychair.org). ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] The CADE-29 ATP System Competition CASC-29
--- CASC-29 - The CADE ATP System Competition to be held at The 29th International Conference on Automated Deduction Rome, Italy, 1st-4th July 2023 The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-29 will be held on the 3rd July 2023, during the 29th International Conference on Automated Deduction. CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of: + the number of problems solved, and + the number of problems solved with a solution output, and + the average runtime for problems solved; in the context of: + a bounded number of eligible problems, chosen from the TPTP library, and + specified time limits for solution attempts. The competition organizer is Geoff Sutcliffe, assisted by Martin Desharnais. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. Further details and registration information are available at: http://www.tptp.org/CASC/29/ Registration of systems for CASC-29 is now invited. System registration closes on 5th June. Please register early so that adequate resources can be allocated. DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! --- ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FroCoS 2023 Call for Papers
CALL FOR PAPERS: FroCoS 2023 The 14th International Symposium on Frontiers of Combining Systems FroCoS 2023 will be held at the Czech Technical University in Prague in September, 2023. FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. The first FroCoS symposium was held in Munich, Germany, in 1996. Initially held every two years, since 2004 it has been organized annually with alternate years forming part of IJCAR. FroCoS 2023 will be co-located with the 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023). Conference website https://frocos2023.github.io Submission link https://easychair.org/conferences/?conf=frocos2023 Important Dates --- Submission of title and abstract: May 11, 2023 Paper submission deadline:May 15, 2023 Notification of acceptance: July 3, 2023 Final version: July 21, 2023 Conference date: September 20-22, 2023 Workshops and Tutorials --- If you would like to organise a workshop or run a tutorial, please let us know before July 14th, 2023. --- Submission Guidelines --- Scope - The program committee seeks high-quality submissions describing original work, written in English, not overlapping with published or simultaneously submitted work to a journal or conference, workshop, symposium, etc. with archival proceedings. Selection criteria include originality of ideas, rigour of evaluation, significance of results, and quality of presentation. The page limit in Springer LNCS style is 15 pages in total excluding references. Papers must be edited in LaTeX using the LLNCS style and must be submitted electronically as PDF files via EasyChair at https://easychair.org/conferences/?conf=frocos2023 For each accepted paper, at least one of the authors is required to register to the symposium and present the work. Formatting instructions and the LLNCS style files can be obtained at http://www.springer.com/br/computer-science/lncs/conference-proceedings-guidelines The FroCoS 2023 conference proceedings will be published in the Springer series Lecture Notes in Artificial Intelligence (LNAI/LNCS) as Gold Open Access under a CC-BY-4.0-license, for a cost of max. 200 Euros per paper, with at least 5 full sponsorships available for authors lacking funds. Details on how to apply for sponsorship will be announced soon. List of Topics -- Topics of interest for FroCoS 2023 include (but are not restricted to): Combinations of logics such as higher-order, first-order, temporal, modal, description or other non-classical logics logics with probability and/or fuzzy measures reasoning procedures, SAT solvers, constraint solving techniques, logical frameworks, deduction methods, and constraint propagation logics for distributed and multi-agent systems term rewriting systems logical reasoning with machine learning logics, reasoning, and natural language processing/semantics programs and specifications and their logical aspects, incl. modularisation Integration of equational and other theories into deductive systems, incl. SMT data structures into constraint logic programming and deduction Modularity of/in logics in term rewriting and the application of any of these, for example for knowledge representation, ontology engineering, and the verification or analysis of information systems. Invited Speakers To be announced Programme Committee (TBC) - Carlos Areces, FaMAF - Universidad Nacional de Córdoba Franz Baader, TU Dresden Peter Baumgartner, CSIRO Clare Dixon, University of Manchester Mathias Fleury, University of Freiburg Didier Galmiche, LORIA - Université de Lorraine Silvio Ghilardi, Università degli Studi di Milano Jürgen Giesl, RWTH Aachen University Andreas Herzig, IRIT at Université Paul Sabatier Jean Christoph Jung, Universität Bremen Roman Kontchakov Birkbeck, University of London Naoki Nishida, Nagoya University Giles Reger, Amazon Web Services and The University of Manchester Andrew Reynolds, The University of Iowa Christophe Ringeissen, LORIA - Université de Lorraine Philipp Ruemmer, Uppsala University Uli Sattler, The University of Manchester (Chair) Renate A. Schmidt, The University of Manchester Roberto Sebastiani, University of Trento Viorica Sofronie-Stokkermans, University Koblenz-Landau K. Subramani, West Virginia University Martin Suda, Czech Technical University in Prague (Chair) Dmitriy Traytel, University of Copenhagen Christoph Weidenbach, Max Planck Institute for Informatics Piotr Wojciechowski, West Virginia University Contact â-- All questions about FroCoS2023 paper submissions should be emailed to the PC Chairs (FroCoS 2023 at easychair.org). Best
[Hol-info] LPAR-24, June 2023, Call for Papers
LPAR-24 Call for Papers LPAR-24 will be held in Manizales, Colombia, at the National University of Colombia, 4-9th June 2023. Details are online at ... https://easychair.org/smart-program/LPAR2023/ The Call for Papers is available at ... https://easychair.org/cfp/LPAR2023 LPAR ... "We boldly go where no reasonable conference has gone before" ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CADE-29 Call for Papers
** CALL FOR PAPERS CADE-29: 29th international Conference on Automated Deduction Sapienza University of Rome Rome, Italy, 1-5 July 2023 https://easyconferences.eu/cade2023 ** -- Overview -- CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including logical foundations, theory and principles, applications in and beyond computer science and mathematics, and implementations of automated reasoning systems are solicited. CADE-29 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction. CADE-29 is in cooperation with ACM SIGLOG. -- Venue -- CADE-29 and affiliated satellite events will take place in Rome, Italy and will be co-located with FSCD 2023. -- Publication -- CADE-29 proceedings will be published in Springer's Lecture Notes in Artificial Intelligence series in Gold Open Access mode at a CADE special rate of â¬200.00 per paper. Funding will be available for authors of accepted papers who cannot cover the â¬200 fee. -- Special Issue -- The authors of a selection of the best CADE-29 papers will be invited to submit an extended version of their paper after the conference, to be published in a special issue of the Journal of Automated Reasoning. -- Submission Guidelines -- Submissions can be made in two categories: - **Regular papers**. Up to 15 pages in LNCS style, excluding references. Proofs of theoretical results that do not fit in the page limit may be provided in an appendix. - **Short papers**. This includes system descriptions, user experiences, case studies and domain models. Up to 10 pages in LNCS style, excluding references. Reviewers may consider material provided in appendices, but submissions must be self-contained within the page limit. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, originality, significance, correctness, and readability. If software or data is relevant to a paper, a link that provides access to the software/data must be provided to enable reproduction of results. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chairs may solicit further reviews after the rebuttal period. Selected accepted papers will be considered by Program Committee for the CADE Best Paper Award. Papers must be submitted to https://easychair.org/conferences/?conf=cade29 All submission must be formatted in the LNCS style and must include the ORCID id of at least the corresponding author, and preferably of all authors. -- Important Dates -- Abstract deadline: February 27, 2023 Submission deadline:March 6, 2023 Rebuttal phase: April 18-20, 2023 Notification: May 3, 2023 Final version: May 24, 2023 Main Conference:July 1-4, 2023 Satellite events: July 4-5, 2023 -- Program Committee Chairs -- Brigitte Pientka, MacGill University Cesare Tinelli, The University of Iowa -- Policies-- CADE implements the ACM policy against harassment. -- Contacts -- All questions about CADE-29 paper submissions should be emailed to the PC Chairs (cade29 at easychair.org). ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Dov Gabbay Prize for Logic and Foundations
Call for Nominations: Dov Gabbay Prize for Logic and Foundations THE PRIZE The ''Dov Gabbay Prize for Logic and Foundations'' is a new international research prize established to honour the extraordinary, multi-faceted scientific contributions of Prof. Dov Gabbay, known among others for editing an extensive collection of Logic Handbooks. It has been launched on the occasion of Dov's 77th birthday this October (Short bio: https://dgp.iloaf.org/dov.html). The prize aims at rewarding outstanding researchers in Logic and Foundations, including Mathematical, Philosophical, and Computational Logic. It pays special attention to work combining - ideally - foundational insight and conceptual innovation with sophisticated theoretical analysis. The winner will receive a cash prize 2001 EUR and be invited to give a talk (accessible for an online audience) at a major logic centre or a logic-related meeting in 2023, depending on the recipient's research area. Specific efforts will be made to promote the rewarded scientific work. NOMINATION Each nomination of a researcher should provide an accessible justification and list the main publications considered relevant. It should also include the name, affiliation, and email address of the nominator. Self-nominations are not allowed, the nominee should not be a hierarchic superior of the nominator. Proposals in pdf-format are to be sent to "dgp[at]iloaf[dot]org". The deadline for this call is January 31, 2023. Early submissions in December are appreciated. DECISION The selection is made by an independent jury consisting of six internationally renowned logicians representing Mathematical, Philosophical, and Computational logic:   Johan van Benthem (Amsterdam University/U Stanford)   Christoph Benzmueller (University of Bamberg)   Agata Ciabattoni (TU Vienna)   Laura Giordano (Università del Piemonte Orientale)   Hannes Leitgeb (LMU Munich)   Philip Welch (University of Bristol) The winner of the 2022 call will be announced in May 2023. ADMIN Prize and process are managed by the "Logic and Foundations Initiative (ILOAF)", which aims at initiating and supporting scientific and educational activities in Logic and Foundations. It is currently sponsored by the Luxembourg Logic Community. CONTACT For any questions, please contact the organizing committee via "dgp[at]iloaf[dot]org". Web: https://dgp.iloaf.org ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Proposals for Sites for IJCAR 2024
Proposals Solicited for Sites for IJCAR 2024 Franz Baader IJCAR Steering Committee Chair franz.baa...@tu-dresden.de We invite proposals for sites around the world to host the 12th International Joint Conference on Automated Reasoning (IJCAR) to be held in summer 2024. Previous IJCAR meetings include IJCAR 2001 in Siena, Italy; IJCAR 2004 in Cork, Ireland; IJCAR 2006 as part of FLoC in Seattle, Washington; IJCAR 2008 in Sydney, Australia; IJCAR 2010 as part of FLoC in Edinburgh, Scotland; IJCAR 2012 in Manchester, UK; IJCAR 2014 as part of the Vienna Summer of Logic in Vienna, Austria; IJCAR 2016 in Coimbra, Portugal; IJCAR 2018 as part of FLoC in Oxford, UK; IJCAR 2020 in Paris, France, as online event; and IJCAR 2022 as part of FLoC in Haifa, Israel. IJCAR is a merger of CADE (Conference on Automated Deduction), TABLEAUX (Conference on Analytic Tableaux and Related Methods), and FroCoS (Symposium on Frontiers of Combining Systems) and possibly other meetings. In 2020, ITP was part of IJCAR and it may join IJCAR again in 2024. Usually, a considerable number of workshops are also affiliated with the conference. The deadline for proposals is January 30, 2023. Proposals should be sent to the IJCAR Steering Committee Chair (see contact information above). We encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within one month after the proposal due date. Proposals should address the following points that also represent criteria for evaluation: * National, regional, and local AR community support: IJCAR Conference Chair and host institution, IJCAR Local Arrangements Committee, availability of (and reward for) student-volunteers. * National, regional, and local government and industry support, both organizational and financial. * Accessibility (i.e., transportation), attractiveness, and desirability of proposed site. * Appropriateness of proposed dates (including consideration of holidays/other events during the period), hotel prices, and access to dormitory facilities (a.k.a. residence halls). * An estimate on registration cost for the conference and workshops, both for regular participants and students. * Conference and exhibit facilities for the anticipated number of registrants (typically up to 200), for example, number, capacity and audiovisual equipment of meeting rooms; a large plenary session room that can hold all the registrants; enough rooms for parallel sessions/workshops/tutorials; Internet connectivity and workstations for demos/competitions; catering services; and presence of professional staff. * Residence accommodation and food services in a range of price categories and close to the conference facilities, for example, number and cost range of hotels, and availability and cost of dormitory rooms (e.g., at local universities) and kind of services they offer. * Rough budget projections for the various budget categories, e.g., cost of renting/cleaning the meeting rooms, if applicable; cost of professional conference secretariat, if hired; and financial model for satellite workshops and/or co-located events. Balance with regard to the geographical distribution of previous IJCAR and its constituent meetings. * For the unlikely case that travel or contact restrictions are again in place: willingness and ability to organize an online or hybrid event. Prospective organizers are encouraged to get in touch with the IJCAR Steering Committee Chair for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] EuroProofNet WG2 kickoff meeting
Dear all, For those that do not yet know EuroProofNet, it is the European research network on digital proofs. EuroProofNet aims at boosting the interoperability and usability of proof systems. You can register here https://europroofnet.github.io/ (follow the link "apply" on the main page). The EuroProofNet Automated Theorem Provers Working Group (WG2) is organizing its kickoff meeting co-located with the 8th Workshop on Practical Aspects of Automated Reasoning (PAAR 2022), taking place at FLoC in Haifa, Israel, at August 11-12, 2022. While PAAR 2022 is a two-day event, the working group meeting will essentially be on the second day of PAAR (August 12). See https://europroofnet.github.io/wg2-meeting1/ and https://paar2022.github.io/ for further details. A preliminary program, including plenary presentations, invited talks and discussion sessions is available at https://europroofnet.github.io/wg2-meeting1/ . The meeting will be primarily in-person, but the organizers plan to implement a hybrid format so that all interested EuroProofNet members can participate via a video call (Details TBA). EuroProofNet can support the in-person participation of WG members. If you want to apply for travel funding support, please send a brief statement about your motivation and topical fit (max. half a page), together with a justified travel cost estimation (e.g., via screenshots or invoices for flights), to Pascal Fontaine and Alexander Steen until the deadline (see below). # Confirmed speakers * Josef Urban * Geoff Sutcliffe * Andres Notzli * Guillaume Burel # Important dates PAAR workshop: August 11-12, 2022 EuroProofNet WG2 meeting: August 12, 2022 Funding request deadline: July 15, 2022 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 14th International Summer School on Verification Technology, Systems & Applications
== First Call for Participation 14th International Summer School on Verification Technology, Systems & Applications http://www.mpi-inf.mpg.de/vtsa22/ The 14th edition of the Summer School on Verification Technology, Systems and Applications (VTSA) will be organized by the Max-Planck-Institute for Informatics Saarbruecken in cooperation with the University of Liege, Inria Nancy - Grand Est, and the University of Luxembourg. The school will take place from September 5th to September 9th, 2022 on Saarland Informatics Campus, Saarbruecken, Germany. The summer school is a joint event with EuroProfNet, COST action CA20111, see https://europroofnet.github.io/. The following speakers have accepted to give courses at VTSA 2022: - Frederic Blanqui: Interoperability of Proof Systems - Carsten Fuhs: Automated Termination and Complexity Analysis of Programs - Andre Platzer: Logic of Autonomous Dynamical Systems - Philipp Ruemmer: Solving Constraints with Complex String Operations - Martina seidl: Reasoning with Quantified Boolean Formulas Participation is free (except for travel and accommodation costs) and open to anybody holding at least a bachelor degree or equivalent in computer science. It includes the lectures, daily coffee breaks and lunches as well as a school dinner. EuroProofNet will refund the travel and accommodation of a number of participants. Please express your interest with your application. Attendance is limited to 40 participants. Please apply electronically by sending to jmuel...@mpi-inf.mpg.de: - a one-page CV, - an application letter explaining your interest in the school and your experience in the area, - a copy of your bachelor certificate (or equivalent or a more significant certificate), - a short statement if you want to contribute to the student sessions - an indication whether you ask EuroProofNet to refund your travel and accommodation (please include your country, university, age and gender as well as your arrival and departure dates and provide an estimate in euros of your transportation costs to Saarbruecken). The deadline for application is July 20th, 2022. Notification of acceptance will be given by July 22nd, 2022. Full details are available at http://www.mpi-inf.mpg.de/vtsa22/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR-11 - Call for participation
The 11th International Joint Conference on Automated Reasoning (IJCAR 2022) August 8-10, in-person in Haifa, Israel The program for IJCAR 2022 is now available at ... https://easychair.org/smart-program/FLoC2022/IJCAR-program.html The workshops assocbiated with IJCAR 2022 are listed at ... https://easychair.org/smart-program/FLoC2022/IJCAR-workshops.html Registration for IJCAR 2022 is now open at ... https://easychair.org/smart-program/FLoC2022/IJCAR-Registration.html Grants to support students' attendance at IJCAR 2022 are available ... https://easychair.org/smart-program/FLoC2022/IJCAR-Grants.html ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] The ALP Alain Colmerauer Prolog Heritage Prize: Call for Nominations
*** Call for Nominations *** The ALP Alain Colmerauer Prolog Heritage Prize Organized by The Association for Logic Programming (ALP) and The Prolog Heritage Association In the summer of 1972, Alain Colmerauer and his team in Marseille developed and implemented the first version of the logic programming language Prolog. Together with both earlier and later collaborations with Robert Kowalski and his colleagues in Edinburgh, this work laid the practical and theoretical foundations for the Prolog and logic programming of today. Prolog and its related technologies soon became key tools of symbolic programming and Artificial Intelligence. The Year of Prolog celebrates the 50th anniversary of these events and highlights the continuing significance of Prolog and Logic Programming both for symbolic, explainable AI, and for computing more generally. This celebration will culminate with the award of the inaugural edition of the ALP Alain Colmerauer Prolog Heritage Prize for recent practical accomplishments that highlight the benefits of Prolog-inspired computing for the future. The Prize will be presented at the Prolog Day Symposium on November 10, 2022, in Paris, France. Eligibility --- Any individual or group of individuals can nominate themselves or their institution(s)/organization(s) for the Prize. Selection - The Prize will be given for depth, novelty, and proven or potential impact. A shortlist of up to five nominations will also be selected in the process. Endowment - The winner(s) will receive a certificate and a cash Prize of 2,000 Euros. The expenses of the shortlisted nominees will be covered up to 1,000 Euros, supported by the Artificial Intelligence Journal. Timeline Deadline for nominations/submissions: *** September 2, 2022 *** Notification of the shortlisted candidates: *** September 30, 2022 *** For more information and details, see https://prologyear.logicprogramming.org/ColmerauerPrize.html The Year of Prolog and its activities, including the Alain Colmerauer Prize, are sponsored by the Association for Logic Programming, the Prolog Heritage Association, the AI Journal, Institut Carnot Cognition, and Institut Fredrik Bull, among others. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Automated Reasoning in Quantified Non-Classical Logics - Call for Papers
ARQNL 2022 - Call for Papers 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (associated with FLoC and IJCAR 2022) 11 August 2022, Haifa, Israel http://iltp.de/ARQNL-2022/ Non-classical logics â such as modal logics, conditional logics, intuitionistic logic, description logics, temporal logics, linear logic, dynamic logic, deontic logics, fuzzy logic, paraconsistent logic, relevance logic â have many applications in AI, Computer Science, Philosophy, Linguistics and Mathematics. Hence, the automation of proof search in these logics is a crucial task. The ARQNL workshop aims at fostering the development of proof calculi, automated theorem proving systems and model finders for all sorts of quantified non-classical logics. The workshop will provide a forum for researchers to present and discuss recent developments in this area. The contributions may range from theory to system descriptions and implementations. Contributions may also outline relevant applications and describe example problems and benchmarks. We welcome contributions from computer scientists, linguists, philosophers, and mathematicians. Research papers (up to 15 pages), or short papers, talk abstracts, and system demonstrations (up to 8 pages) are solicited. The submission deadline is May 6th. The ARQNL Proceedings will be published in the CEUR Workshop Proceedings. For further information see the workshop website at http://iltp.de/ARQNL-2022/. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Bill McCune PhD Award 2021 - Call for Nominations
Title: Bill McCune PhD Award in Automated Reasoning, Call for Nominations *** Automated Reasoning is the area of Computer Science dedicated to applying reasoning in the form of logic to computing systems. The Bill McCune PhD Award in Automated Reasoning distinguishes each year a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. The award is named after the American computer scientist William Walker McCune, known for his contributions in the fields of Automated Reasoning, Algebra, Logic, and Formal Methods. He was the implementer of OTTER, Prover9 and Mace 4, automated tools for first-order reasoning which are known to this day for their accuracy and robustness. He was also known for his generosity towards research colleagues and as a great supporter of young researchers in the field. * Eligibility * Eligible for the award are those who successfully defended their PhD - at an academic institution; - in the field of Automated Reasoning; and - in the period from January 1, 2021 - December 31, 2021. The PhD students supervised by the Expert Committee members are not eligible. * Nomination * Candidates for the award must be nominated by their supervisor(s) and one additional independent researcher who reviewed/examined the thesis. Nominations are to be submitted via email sent to both na...@unb.br and pascal.fonta...@uliege.be, by April 15, 2022. The nomination must consist of one compressed file (.zip) containing: - a letter from the supervisor(s) describing why the thesis should be considered for the award and the relationship of the contributions to CADE/IJCAR; - a report from the nominating additional independent researcher who reviewed/examined the thesis; - the thesis itself; - a copy of the PhD diploma; and - a copy of relevant papers by the nominee, if any, containing results published in the thesis. * Procedure * The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated Reasoning. - The nominations will be evaluated and compared by an international Expert Committee (see below). - The procedure to be followed is analogous to the review phase of a conference. The justification by the supervisor and the nominating additional independent researcher report will play an important role in the evaluation. - The final decision is made by the Expert Committee at least one month before CADE/IJCAR is being held. - The award consists of a certificate announcing the winner to have received the Bill McCune PhD Award in Automated Reasoning. The award will be announced at the respective year's CADE/IJCAR. The nominators of the winner will also receive a copy of this certificate. The recipient of the award is expected to attend the award ceremony. - The decision of the Expert Committee is final and binding, and not subject to discussion. * Expert Committee * The Expert Committee, consisting of leading researchers in Automating Reasoning, is formed by the board of CADE Trustees with the aim to reflect the broad diversity in the area of Automated Reasoning. It is announced with the call for nominations, and thus formed before this call. The decision on the award is taken by the Expert Committee. The Expert Committee can seek additional expertise, even after the submission deadline for nominations. Expert Committee members cannot nominate a PhD student. Expert Committee members cannot contribute an independent report seconding a nomination. The Expert Committee for the Bill McCune PhD Award 2021 consists of the following people: - Nikolaj Bjorner, Microsoft - Pascal Fontaine, University of Liege - Carsten Fuhs, Birkbeck, University of London - Marijn Heule, Carnegie Mellon University - Claudia Nalon, University of Brasilia - Andrew Reynolds, The University of Iowa - Philipp Ruemmer, Uppsala University - Martina Seidl, Johannes Kepler University - Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau - Rene Thiemann, University of Innsbruck *** ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 8TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING - Call for Papers
CALL FOR PAPERS PAAR 2022: 8TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING -- co-located with FLoC/IJCAR 2022 -- August 11-12, 2022, Haifa, Israel Web site: https://paar2022.github.io/ Submission link: https://easychair.org/conferences/?conf=paar2022 Abstract registration deadline: April 19, 2022 Submission deadline: April 26, 2022 ** Description ** The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well-behaved in practice, and connect well to application domains? which reasoning tasks are tractable and useful? which algorithms are able to solve real-world instances? how should automated reasoning tools be designed, implemented, tested, and evaluated? The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies. PAAR 2022 will host the meeting of the working group on Automated Theorem Provers of the EuroProofNet COST action (https://europroofnet.github.io/). Every workshop participant is welcome to attend. ** Submission Guidelines ** Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages), excluding references, via EasyChair at https://easychair.org/conferences/?conf=paar2022. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. Submissions should be prepared in LaTeX using the EasyChair proceedings style. The package containing the class file and its user guide and some helper tools can be downloaded from http://www.easychair.org/publications/easychair.zip. ** SCOPE ** Topics include, but are not limited to: -- * automated reasoning in propositional, first-order, higher-order, and non-classical logics; * implementation of provers (SAT, SMT, resolution, superposition, tableau, instantiation-based, rewriting, logical frameworks, etc.); * automated reasoning tools for all kinds of practical problems and applications; * pragmatics of automated reasoning within proof assistants; * practical experiences, usability aspects, feasibility studies; * evaluation of implementation techniques and automated reasoning tools; * performance aspects, benchmarking approaches; non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications; * implementation techniques, optimisation techniques, machine learning, strategies and heuristics, fairness; * tools or methods that support prover development; * system descriptions and demos. ** Programme Committee ** * Boris Konev, University of Liverpool, UK (PC co-chair) * Claudia Schon, University of Koblenz-Landau, DE (PC co-chair) * Alexander Steen, University of Greifswald, DE (PC co-chair) * Simon Cruanes, Imandra, US * Hans de Nivelle, Nazarbayev University, KZ * Gabriel Ebner, Vrije Universiteit Amsterdam, NL * Pascal Fontaine, Université de Liège, BE * Ulrich Furbach, University of Koblenz, DE * Cezary Kaliszyk, University of Innsbruck, AT * Daniel Le Berre, CNRS - Université d'Artois, FR * Ondrej Lengal, Brno University of Technology, CZ * Tomer Libal, American University of Paris, FR and University of Luxembourg, LU * Cláudia Nalon, University of BrasÃlia, BR * Jens Otten, University of Oslo, NO * Philipp Ruemmer, Uppsala University, SE * Renate A. Schmidt, The University of Manchester, UK * Stephan Schulz, DHBW Stuttgart, DE * Mihaela Sighireanu, ENS Paris-Saclay and CNRS, FR * Frieder Stolzenburg, Harz University of Applied Sciences, DE * Martin Suda, Czech Technical University in Prague, CZ * Sophie Tourret, Inria and MPI for Informatics, DE * Petar VukmiroviÄ, Vrije Universiteit Amsterdam, NL * Sarah Winkler, Free University of Bolzano-Bozen, IT * Aleksandar ZeljiÄ, Stanford University, US ** Publication ** PAAR proceedings will be published electronically in the CEUR workshop proceedings. ** Venue ** FLoC 2022 at Haifa, Israel ** Important dates ** * Abstract submission: April 19, 2022 * Paper submission: April 26, 2022 * Workshop: August 11 - August 12, 2022 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] TAP22: Tests and Proofs 2022 - Call for Papers
TAP22: Tests and Proofs 2022 co-located event of STAF 2022 Nantes, France, July 4-8, 2022 Conference website https://easychair.org/smart-program/TAP22/index.html Submission link https://easychair.org/conferences/?conf=tap22 Conference program https://easychair.org/smart-program/TAP22/ Abstract registration deadline March 18, 2022 Submission deadline March 23, 2022 Author notification May 9, 2022 The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability. Research in verification has seen a steady convergence of heterogeneous techniques and a synergy between the traditionally distinct areas of testing (and dynamic analysis) and of proving (and static analysis). Formal techniques for counter-example generation based on, for example, symbolic execution, SAT/SMT-solving or model checking, furnish evidence for the potential of a combination of tests and proofs. The combination of predicate abstraction with testing-like techniques based on exhaustive enumeration opens the perspective for novel techniques of proving correctness. On the practical side, testing offers cost-effective debugging techniques of specifications or crucial parts of program proofs (such as invariants). Last but not least, testing is indispensable when it comes to the validation of the underlying assumptions of complex system models involving hardware and/or system environments. Over the years, there is growing acceptance in research communities that testing and proving are complementary rather than mutually exclusive techniques. The TAP conference aims to promote research in the intersection of testing and proving by bringing together researchers and practitioners from both areas of verification. *** Submission Guidelines All papers must be original and not simultaneously submitted to another journal or conference. The following paper categories are welcome: ** Regular research papers: full submissions describing original research, of up to 16 pages (excluding references and appedix). In case regular papers rely on experimental data and/or tool support, authors are strongly recommended to make the experimental data and/or tool support available for public use. ** Tool demonstration papers: submissions describing the design and implementation of an analysis/verification tool or framework, of up to 8 pages (excluding references and appendix). The tool/framework described in a tool demonstration paper should be available for public use. ** Short papers: submissions describing preliminary findings, proofs of concepts, and exploratory studies, of up to 6 pages (excluding references and appendix). Papers have to adhere to Springer's LNCS format and must be submitted in PDF format at the EasyChair submission site: https://easychair.org/conferences/?conf=tap22 *** List of Topics TAP's scope encompasses many aspects of verification technology, including foundational work, tool development, and empirical research. Its topics of interest center around the connection between proofs (and other static techniques) and testing (and other dynamic techniques). Papers are solicited on, but not limited to, the following topics: * Verification and analysis techniques combining proofs and tests * Program proving with the aid of testing techniques * Deductive techniques supporting the automated generation of test vectors and oracles (theorem proving, model checking, symbolic execution, SAT/SMT solving, constraint logic programming, etc.) * Deductive techniques supporting novel definitions of coverage criteria * Program analysis techniques combining static and dynamic analysis * Specification inference by deductive and dynamic methods * Testing and runtime analysis of formal specifications * Search-based technics for proving and testing * Verification of verification tools and environments * Applications of test and proof techniques in new domains, such as security, configuration management, learning * Combined approaches of test and proof in the context of formal certifications (Common Criteria, CENELEC, â¦) * Case studies, tool and framework descriptions, and experience reports combining tests and proofs *** Program Committee * Wolfgang Ahrendt (Chalmers University of Technology) * Catherine Dubois (ENSIIE-Samovar) * Carlo A. Furia (USI - Università della Svizzera Italiana) * Dilian Gurov (KTH Royal Institute of Technology) * Falk Howar (TU Clausthal / IPSSE) * Marieke Huisman (University of Twente) * Reiner Hähnle (TU Darmstadt) * Einar Broch Johnsen (University of Oslo) * Konstantin Korovin (The University of Manchester) * Laura Kovacs (Vienna University of Technology) - chair * Karl Meinke (KTH Royal Institute of Technology) - chair * Jakob Nordstrom (University of
[Hol-info] iPRA 2022 - 4th Workshop on Interpolation: from Proofs to Applications
iPRA 2022 - FOURTH WORKSHOP ON INTERPOLATION: FROM PROOFS TO APPLICATIONS CALL FOR CONTRIBUTIONS Workshop date: August 11, 2022 Location:Haifa, Israel Web: https://ipra-2022.bitbucket.io/ iPRA 2022 is a workshop at the Federated Logic Conference (FLoC) 2022 IMPORTANT DATES Submission deadline: May 10, 2022, AOE Author notification: June 1, 2022 Workshop:August 11, 2022 SCOPE Starting from Craig's interpolation theorem for first-order logic, the existence and computation of interpolants became an active research area, with applications in different fields, notably in verification, databases, and knowledge representation. There are challenging theoretical and practical questions, for model-theoretic as well as proof-theoretic approaches. The workshop aims at bringing together researchers working on interpolation and its various applications, based on different approaches, increasing the awareness of the automated reasoning community for challenging open problems related to interpolation. The workshop will include invited talks, invited tutorials (speakers to be announced), and contributed talks. For the contributed talks, we solicit submissions in the form of abstracts. The authors of accepted abstracts are required to present their work at the workshop. A book of abstracts will be published online in advance of the event. We encourage submissions presenting work in progress, tools under development, as well as research of PhD students, such that the workshop can become a forum for active dialog. Presentations of recently published papers are also allowed and encouraged, but please indicate on your submission where the paper was published/presented. Relevant topics include, but are not limited to: - Applications of interpolation - Complexity results and limitations - Definability and interpolation - Generalizations of Craig interpolation - Inductive proofs - Interpolating decision procedures - Interpolation-based invariant generation - Interpolation procedures and algorithms - Logical abduction - Practical methods for interpolation - Program analysis and verification - Proof systems and calculi for interpolation - Proof transformation techniques - Relating model theoretic and proof theoretic approaches - Separability - Uniform interpolation PROGRAMME COMMITTEE Michael Benedikt (University of Oxford, UK) - co-chair Maria Paola Bonacina (Universita degli Studi di Verona, Italy) Silvio Ghilardi (Universita degli Studi di Milano, Italy) Arie Gurfinkel (University of Waterloo, Canada) Laura Kovacs (TU Wien, Austria) Rosalie Iemhoff (Utrecht University, The Netherlands) Pavel Pudlak (Czech Academy of Sciences, Czech Republic) Philipp Ruemmer (Uppsala University, Sweden) - co-chair Georg Weissenbacher (TU Wien, Austria) Christoph Wernhard (University of Potsdam, Germany) - co-chair Frank Wolter (University of Liverpool, UK) SUBMISSION INSTRUCTIONS Abstracts (at most one page, excluding references) or extended abstracts (at most 5 pages, excluding references) have to be submitted by the submission deadline. Submissions should be written in English, and preferably formatted in the style of the Springer Publications format for Lecture Notes in Computer Science (LNCS). Papers should be submitted electronically via https://easychair.org/conferences/?conf=ipra2022 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 17th Workshop on Logical and Semantic Frameworks with Applications - LSFA 2022 - Call for Papers
17th Workshop on Logical and Semantic Frameworks with Applications - LSFA 2022 23-24 September 2022 https://lsfa2022.dcc.ufmg.br/ Belo Horizonte, Brazil First Call For Papers ***Overview*** Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and computational languages, supporting tool development and reasoning. The LSFA series' objective is to put together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and use of such techniques and results, from the practical side. See lsfa.cic.unb.br for more information. LSFA topics of interest include, but are not limited to: * Automated deduction * Applications of logical and semantic frameworks * Computational and logical properties of semantic frameworks * Formal semantics of languages and systems * Implementation of logical and semantic frameworks * Lambda and combinatory calculi * Logical aspects of computational complexity * Logical frameworks * Process calculi * Proof theory * Semantic frameworks * Specification languages and meta-languages * Type theory ***Submissions*** Contributions should be written in English and submitted in full paper (with a maximum of 16 pages excluding references) or short papers (with a maximum of 6 pages excluding references). They must be unpublished and not submitted simultaneously for publication elsewhere. The papers should be prepared in LaTeX using the EPTCS style. The submission should be in the form of a PDF file uploaded to Easychair:  https://easychair.org/conferences/?conf=lsfa2022 The pre-proceedings, containing the reviewed papers, will be available at the LSFA's webpage. After the meeting, the authors will be invited to submit full versions of their works for the post-proceedings publication. At least one of the authors of each submission must register for the conference. Presentations should be in English. According to the submissions' quality, the chairs will promote the further publication of journal revised versions of the papers. Previous LSFA Special Issues have been published in journals such as The Logical J. of the IGPL, Theoretical Computer Science and Mathematical Structures in Computer Sciences (see the LSFA page http://lsfa.cic.unb.br). ***Important dates*** * Abstract: Monday 2 May * Submission: Monday 9 May * Notification: Saturday 9 July * Preliminary proceedings version due: Thursday 1 September * Conference: Friday-Saturday 23-24 September * Submission for final EPTCS proceedings: Monday 17 October * Final version: Monday 21 November ***Program Committee*** Beniamino Accattoli, Inria & Ãcole Polytechnique, France Sandra Alves, Universidade de Porto, Portugal Carlos Areces, Universidad Nacional de Córdoba, Argentina Mauricio Ayala Rincón, Universidade de BrasÃlia, Brazil Haniel Barbosa, Universidade Federal de Minas Gerais, Brazil Mario R. Folhadela Benevides, Universidade Federal Fluminense, Brazil Alejandro DÃaz-Caro, Universidad Nacional de Quilmes & ICC, CONICET/Universidad de Buenos Aires, Argentina Amy Felty, University of Ottawa, Canada Pascal Fontaine, University of Liège, Belgium (co-chair) Edward Hermann Haeusler, PUC-Rio de Janeiro, Brazil Delia Kesner, Université de Paris, France Temur Kutsia, RISC/Johannes Kepler University Linz, Austria Bruno Lopes, Universidade Federal Fluminense, Brazil Ian Mackie, Polytechnique, France, and University of Sussex, UK Alexandre Madeira, Universidade de Aveiro, Portugal Sérgio Marcelino, University of Lisbon, Portugal Mariano Moscato, National Institute of Aerospace, USA Daniele Nantes, Universidade de BrasÃlia, Brazil (co-chair) Vivek Nigam, Huawei Munich Research Center, Germany Carlos Olarte, Université Sorbonne Paris Nord, France Mateus de Oliveira Oliveira, University of Bergen, Norway Valeria de Paiva, Topos Institute, Berkeley, USA, Brazil Alberto Pardo, Universidad de la República, Uruguay Elaine Pimentel, University College London, UK Giselle Reis, Carnegie Mellon University-Qatar, Qatar Umberto Rivieccio, Universidade Federal do Rio Grande do Norte, Brazil Camilo Rocha, Pontificia Universidad Javeriana - Cali, Colombia Daniel Ventura, Universidade Federal de Goiás, Brazil Petrucio Viana, Universidade Federal Fluminense, UFF, Brazil ***Organisers*** Haniel Barbosa (UFMG, Brazil) Mario S. Alvim (UFMG, Brazil) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2022 - Extended Deadline
IJCAR is the premier international joint conference on all aspects of automated reasoning. IJCAR 2022 is the 11th edition of IJCAR. It will be held in Haifa (Israel), August 7-12, 2022, as part of FLoC 2022. IJCAR 2022 is the merger of the following conferences in automated reasoning: + CADE (Conference on Automated Deduction) + FroCoS (Symposium on Frontiers of Combining Systems) + TABLEAUX (Conference on Analytic Tableaux and Related Methods) For more details about the conference, venue and organization, see the conference webpage: https://easychair.org/smart-program/FLoC2022/IJCAR-index.html THE SUBMISSION DEADLINE HAS BEEN EXTENDED TO 18th FEBRUARY See the CFP at ... https://easychair.org/cfp/IJCAR-2022 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2022 - Call for Papers
IJCAR is the premier international joint conference on all aspects of automated reasoning. IJCAR 2022 is the 11th edition of IJCAR. It will be held in Haifa (Israel), August 7-12, 2022, as part of FLoC 2022. IJCAR 2022 is the merger conference of the following leading events in automated reasoning: + CADE (Conference on Automated Deduction) + FroCoS (Symposium on Frontiers of Combining Systems) + TABLEAUX (Conference on Analytic Tableaux and Related Methods) For more details about the conference, venue and organization, see the conference webpage: https://easychair.org/smart-program/FLoC2022/IJCAR-index.html *** Submission Guidelines IJCAR 2022 invites submissions related to all aspects of automated or interactive reasoning, including foundations, implementations, and applications. All papers must be original and not simultaneously submitted to another journal or conference. The following paper categories are welcome: + Regular papers describing solid new research results. They can be up to 16 pages long, including figures but excluding references and appendices. Where applicable, regular papers are supported by experimental validation. Submissions reporting on case studies in an industrial context are strongly invited as regular papers, and should describe details, weaknesses and strength in sufficient depth. + System description papers describing implementations of systems, reporting on novel features and experiments with implemented systems. System description papers can be up to 7 pages long, including figures but excluding references and appendices. System description papers should also be supported by a link to the artifact/experimental evaluation available to the reviewers. Each of these papers should mention the phrase "(system description)" beneath the title. Papers describing tools that have already been presented in other conferences before will be accepted only if significant and clear enhancements to the tool are reported and implemented. Both types of papers must be formatted using the Springer LNCS styles and submitted in PDF via EasyChair: https://easychair.org/conferences/?conf=ijcar2022 Authors of accepted papers are required to ensure that at least one of them will present the paper at the conference. IJCAR 2022 proceedings will be published in the Springer LNCS series. Springer encourages authors to include their ORCIDs in their papers. *** List of Topics + Logics of interest include: propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, type theory. + Methods of interest include: tableaux, sequent calculi, resolution, model- elimination, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, automated theorem proving, combination of decision or proof procedures, SAT and SMT solving, integration of proof assistants with automated provers and other symbolic tools, etc. + Applications of interest include: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, education, formalization of mathematics etc. *** Program Committee Jasmin Blanchette (Vrije Universiteit Amsterdam) - chair Laura Kovacs (Vienna University of Technology) - chair Dirk Pattinson (The Australian National University) - chair Erika Abraham (RWTH Aachen University) Carlos Areces (FaMAF - Universidad Nacional de Córdoba) Bernhard Beckert (Karlsruhe Institute of Technology) Alexander Bentkamp (Vrije Universiteit Amsterdam) Armin Biere (Albert-Ludwigs-Universität Freiburg) Nikolaj Bjørner (Microsoft) Frédéric Blanqui (INRIA) Maria Paola Bonacina (Università degli Studi di Verona) Kaustuv Chaudhuri (INRIA) Agata Ciabattoni (Vienna University of Technology) Stéphane Demri (CNRS, LMF, ENS Paris-Saclay) Clare Dixon (University of Manchester) Huimin Dong (Sun Yat-Sen University) Katalin Fazekas (TU Wien) Mathias Fleury (University of Freiburg) Pascal Fontaine (Université de Liège, Belgium) Nathan Fulton Silvio Ghilardi (Dipartimento di Matematica, Università degli Studi di Milano) Jürgen Giesl (RWTH Aachen University) Rajeev Gore (The Australian National University) Marijn Heule (Carnegie Mellon University) Radu Iosif (Verimag, CNRS, University of Grenoble Alpes) Mikolas Janota (Czech Technical University in Prague) Moa Johansson (Chalmers University of Technology) Cezary Kaliszyk (University of Innsbruck) Orna Kupferman (Hebrew University) Cláudia Nalon (University of BrasÃlia) Vivek Nigam (Huawei ERC) Tobias Nipkow (Technical University of Munich) Jens Otten (University of Oslo) Nicolas Peltier (CNRS
[Hol-info] 2022 Alonzo Church Award: Call for Nominations
CALL FOR NOMINATIONS The 2022 Alonzo Church Award for Outstanding Contributions to Logic and Computation INTRODUCTION An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Goedel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see https://siglog.org/alonzo-church-award/, https://www.eatcs.org/index.php/church-award/, and https://www.eacsl.org/alonzo-church-award/ . The 2021 Alonzo Church Award was given jointly to Georg Gottlob, Christoph Koch, Reinhard Pichler, Luc Segoufin and Klaus U. Schulz for their ground- breaking work on logic-based web-data extraction, and querying tree-structured data. Lists containing this and all previous winners can be found through the links above. ELIGIBILITY AND NOMINATIONS The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2022 award, the cut-off date is January 1, 1997. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Goedel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference. Nominations for the 2022 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self- nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness. Nominations should be submitted to rjaga...@depaul.edu by April 2, 2022. PRESENTATION OF THE AWARD The 2022 award will be presented at the Federated Logic Conference 2022, which is scheduled to take place in Haifa, Israel in July/August 2022. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared. AWARD COMMITTEE The 2022 Alonzo Church Award Committee consists of the following five members: Thomas Colcombet, Mariangiola Dezani, Javier Esparza, Radha Jagadeesan (chair), and Igor Walukiewicz. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2022 - Call for Papers
IJCAR 2022 - Call for Papers https://easychair.org/smart-program/IJCAR2022/. ***Important Dates*** Submission deadline February 11, 2022 Start of authors response periodApril 16, 2022 End of authors response period April 18, 2022 Authors notificationApril 25, 2022 Overview* IJCAR is the premier international joint conference on all aspects of automated reasoning. IJCAR 2022 is the 11th edition of IJCAR. It will be held in Haifa (Israel), during August 7-12, 2022, as part of FLoC 2022. IJCAR 2022 is the merger conference of the following leading events in automated reasoning: CADE (Conference on Automated Deduction) FroCoS (Symposium on Frontiers of Combining Systems) TABLEAUX (Conference on Analytic Tableaux and Related Methods) Submission Guidelines IJCAR 2022 invites submissions related to all aspects of automated or interactive reasoning, including foundations, implementations, and applications. All papers must be original and not simultaneously submitted to another journal or conference. The following paper categories are welcome: - Regular papers describing solid new research results. They can be up to 16 pages long, including figures but excluding references and appendices. Where applicable, regular papers are supported by experimental validation. Submissions reporting on case studies in an industrial context are strongly invited as regular papers, and should describe details, weaknesses and strength in sufficient depth. - System description papers describing implementations of systems, reporting on novel features and experiments with implemented systems. System description papers can be up to 7 pages long, including figures but excluding references and appendices. System description papers should also be supported by a link to the artifact/experimental evaluation available to the reviewers. Each of these papers should mention the phrase ``(system description)" beneath the title. Papers describing tools that have already been presented in other conferences before will be accepted only if significant and clear enhancements to the tool are reported and implemented. Both types of papers must be formatted using the Springer LNCS styles and submitted in PDF via EasyChair: https://easychair.org/conferences/?conf=ijcar2022 Authors of accepted papers are required to ensure that at least one of them will present the paper at the conference. List of Topics IJCAR 2022 topics include the following ones: * Logics of interest include: propositional, first-order, classical, equational, higher-order, non-classical, constructive, modal, temporal, many-valued, substructural, description, type theory. * Methods of interest include: tableaux, sequent calculi, resolution, model- elimination, inverse method, paramodulation, term rewriting, induction, unification, constraint solving, decision procedures,model generation, model checking, semantic guidance, interactive theorem proving, logical frameworks, AI-related methods for deductive systems, proof presentation, automated theorem proving, combination of decision or proof procedures, SAT and SMT solving, integration of proof assistants with automated provers and other symbolic tools, etc. * Applications of interest include: verification, formal methods, program analysis and synthesis, computer mathematics, declarative programming, deductive databases, knowledge representation, education, formalization of mathematics etc. Publication IJCAR 2022 proceedings will be published in the Springer LNCS series. Springer encourages authors to include their ORCIDs in their papers. Conference Chair Arnon Avron (Tel-Aviv University) Program Committee Chairs Jasmin Blanchette (Vrije Universiteit Amsterdam) - chair Laura Kovacs (Vienna University of Technology) - chair Dirk Pattinson (The Australian National University) - chair Workshop Chairs Simon Robillard (Université de Montpellier) Sophie Tourret (Max Planck Institute for Informatics)) Tutorials and Competition Chair Yoni Zohar (Stanford University) Publicity Chair Geoff Sutcliffe (University of Miami) Program Commitee Erika Abraham (RWTH Aachen University) Carlos Areces (FaMAF - Universidad Nacional de Córdoba) Bernhard Beckert (Karlsruhe Institute of Technology) Alexander Bentkamp (Vrije Universiteit Amsterdam) Armin Biere (Albert-Ludwigs-Universität Freiburg) Nikolaj Bjørner (Microsoft) Jasmin Blanchette (Vrije Universiteit Amsterdam) Frédéric Blanqui (INRIA) Maria Paola Bonacina (Università degli Studi di Verona) Kaustuv Chaudhuri (INRIA) Agata Ciabattoni (Vienna University of Technology) Stéphane Demri (CNRS, LMF, ENS Paris-Saclay) Clare Dixon (University of Manchester) Huimin Dong (Sun Yat-Sen University) Katalin Fazekas (TU Wien) Mathias Fleury (University of Freiburg) Pascal Fontaine (Université de Liège, Belgium) Nathan Fulton
[Hol-info] IJCAR 2022 - Call for Workshops
IJCAR 2022: call for workshops 11th International Joint Conference on Automated Reasoning â IJCAR 2022 August 7â12, 2022, Haifa, Israel, part of FLoC 2022, https://easychair.org/smart-program/IJCAR2022/ The International Joint Conference on Automated Reasoning (IJCAR 2022), part of the Eighth Federated Logic Conference (FLoC 2022), is soliciting proposals for workshops, tutorials and competitions. Researchers are invited to submit proposals on any topic related to automated reasoning, from theoretical foundations to tools and applications. The workshops and tutorials will take place before and after the FLoC conferences: * Sunday & Monday, July 31âAugust 1, 2022, and * Thursday & Friday, August 11â12, 2022. (Note that IJCAR will take place on August 7-10, 2022. We recommend that you plan your event on the second period, and indicate it in the proposal.) Proposals for all conferences affiliated to FLoC, including IJCAR, will be reviewed jointly. Please make sure that the proposal indicates an affiliation to IJCAR. Proposals must be submitted before September 27, 2021. For further details about the submission process and the expected content of workshop and tutorial proposals, see https://floc2022.org/workshops/ . Competition proposals should be sent directly to Yoni Zohar at yoni...@gmail.com . ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CLAR 2021 - Deadline Extension
-- Fourth International Conference on Logic and Argumentation (CLAR 2021) 20-22 October 2021, Hangzhou, China Hybrid (physical or virtual attendance) https://www.xixilogic.org/events/clar2021 -- Following some requests, the submission deadline for CLAR 2021 has been extended. Please find below the updated important dates. *Important Dates* Submission: 11 July 2021 Notification: 13 August 2021 Camera-Ready: 23 August 2021 Conference: 20-22 October 2021 The 4th International Conference on Logic and Argumentation (CLAR 2021) invites contributions from logic, artificial intelligence, philosophy, computer science, linguistics, law, and other areas studying logic and formal argumentation. CLAR 2021 will be held in Hangzhou, 20-22 October 2021 at *Zhejiang University City College*: http://english.zucc.edu.cn/ Due to the uncertainties of the epidemiological situation, the conference will be held in a HYBRID format (virtual and physical attendance both accepted), and we encourage physical participation if possible. Papers accepted to CLAR 2021 will be published as Springer LNAI proceedings, and will be available online during the conference. Authors of selected papers will be invited to submit an extended version to a journal special issue after the conference. More information about CLAR 2021 can be found at the conference website: http://www.xixilogic.org/events/clar2021 The CLAR 2021 conference will highlight recent advances in logic and argumentation and foster interaction between these areas within and outside China. Previous conferences can be accessed via: http://www.xixilogic.org/events/clar *List of Topics* Suggested topics include, but are not limited to the following: * Abstract argumentation * Applications of logic and/or argumentation * Applied logic * Argumentation and game theory * Argumentation and law * Argumentation and linguistics * Argumentation and medical reasoning * Argumentation in AI * Argument mining * Argumentation schemes * BDI logic * Computational argumentation * Deontic logic * Dynamic epistemic logic and belief revision * Formal models for dialog and argumentation * Informal logic * Judgment aggregation * Knowledge representation and reasoning * Logic for game theory * Logic for multi-agent systems * Logic for semantic web * Logic for social network * Mathematical logic * Modal logic * Nonmonotonic logics * Numerical and uncertainty reasoning * Philosophical logic * Pragma-Dialectics * Preference logic * Structured argumentation * Uncertain argumentation *Submission Guidelines* We invite two types of submissions: full papers (12 - 20 pages) describing original and unpublished work and extended abstracts (5 - 8 pages) of preliminary original work or extended abstracts of already published work (needs to be highlighted along with the title), from either the field of logic or the field of formal argumentation. Additional support material may be included in an appendix, which may be considered or ignored by the program committee. Submissions must be prepared in LaTeX, using the Springer LNCS style: ftp://ftp.springernature.com/cs-proceeding/llncs/llncs2e.zip Submissions not complying with these guidelines will be desk rejected. Papers in PDF format should be submitted via EasyChair: https://easychair.org/conferences/?conf=clar2021 Each submitted paper will be carefully peer-reviewed by a panel of PC members based on originality, significance, technical soundness, clarity of exposition and relevance for the conference. For each accepted paper, at least one author is expected to register and present the paper at the conference. *Invited Speakers* Anette Frank (Heidelberg University, DE) Giovanni Sartor (University of Bologna & the EUI, IT) Ken Satoh (NII and Sokendai, JP) Guillermo Simari (Universidad Nacional del Sur, AR) Minghui Xiong (Sun Yat-sen University, CN) *PC Chairs* Pietro Baroni, University of Brescia Christoph Benzmüller, Freie Universität Berlin Yì N. Wáng, Sun Yat-sen University For general questions or questions regarding the local organizations please send emails to clar2...@xixilogic.org. Questions regarding the program should go to the PC chairs directly. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FroCoS 2021 - Final Call for Papers
FINAL CALL FOR PAPERS: FroCoS 2021 == The 13th International Symposium on Frontiers of Combining Systems FroCoS 2021 will be held in the University of Birmingham on September 6-9, 2021. FroCoS is the main international event for research on the development of techniques and methods for the combination and integration of formal systems, their modularization and analysis. The first FroCoS symposium was held in Munich, Germany, in 1996. Initially held every two years, since 2004 it has been organized annually with alternate years forming part of IJCAR. FroCoS 2021 will be co-located with the 29th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2021). Conference website https://frocos2021.github.io Submission link https://easychair.org/conferences/?conf=frocos2021 Abstract registration deadline April 26, 2021 Submission deadline May 3, 2021 Important Dates --- Submission of title and abstract: April 26 Paper submission deadline: May 3 Notification of acceptance: June 18 Final version: 7 July Conference date: September 8-10 Submission Guidelines Scope - The program committee seeks high-quality submissions describing original work, written in English, not overlapping with published or simultaneously submitted work to a journal or conference with archival proceedings. Selection criteria include accuracy and originality of ideas, clarity and significance of results, and quality of presentation. The page limit in Springer LNCS style is 15 pages in total excluding references. Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via EasyChair at https://easychair.org/conferences/?conf=frocos2021 For each accepted paper, at least one of the authors is required to register to the symposium and present the work. Formatting instructions and the LNCS style files can be obtained at http://www.springer.com/br/computer-science/lncs/conference-proceedings-guidelines The FroCoS 2021 conference proceedings will be published in the Springer series Lecture Notes in Artificial Intelligence (LNAI/LNCS). List of Topics -- Topics of interest for FroCoS 2021 include (but are not restricted to): - Combinations of logics (such as higher-order, first-order, temporal, modal, description or other non-classical logics) - Combination and integration methods in SAT and SMT solving - Combination of decision procedures, satisfiability procedures, constraint solving techniques, or logical frameworks - Combination of logics with probability and/or fuzzy measures - Combinations and modularity in ontologies - Integration of equational and other theories into deductive systems - Hybrid methods for deduction, resolution and constraint propagation - Hybrid systems in knowledge representation and natural language semantics - Combined logics for distributed and multi-agent systems - Logical aspects of combining and modularizing programs and specifications - Integration of data structures into constraint logic programming and deduction - Combinations and modularity in term rewriting - Methods and techniques for the verification and analysis of information systems - Methods and techniques for combining logical reasoning with machine learning Invited Speakers - Michael Benedikt Oxford University - Vijay Ganesh University of Waterloo - Chantal Keller LMF, Université Paris-Saclay - Renate Schmidt (joint with TABLAUX) Manchester University Programme Committee --- - Takahito Aoto Niigata University - Carlos Areces FaMAF - Universidad Nacional de Córdoba - AlessandroArtale Free University of Bozen-Bolzano - Franz Baader TU Dresden - Peter Baumgartner CSIRO - Christoph Benzmüller Freie Universität Berlin - Jasmin Blanchette Vrije Universiteit Amsterdam - Clare Dixon University of Manchester - Pascal Fontaine Université de Liège, Belgium - Didier Galmiche LORIA - Université de Lorraine - Silvio Ghilardi Universita degli Studi di Milano - Jürgen Giesl RWTH Aachen University - Andreas HerzigIRIT at Université Paul Sabatier - Jean Christoph Jung Universität Bremen - Boris Konev University of Liverpool (Chair) - Roman Kontchakov Birkbeck, University of London - Aina Niemetz Stanford University - Andrei PopescuUniversity of Sheffield - Silvio Ranise University of Trento and Fondazione Bruno Kessler, Trento, Italy - Giles Reger The University of Manchester (Chair) - Andrew Reynolds The University of Iowa - Christophe Ringeissen LORIA - Université de Lorraine - Philipp Ruemmer Uppsala University - Uli Sattler
[Hol-info] AITP 2021 - Call for Contributions
CALL FOR CONTRIBUTIONS Artificial Intelligence and Theorem Proving AITP 2021 September 5-10, 2021, Aussois and online, France http://aitp-conference.org/2021 Deadline: May 5, 2021 https://easychair.org/my/conference?conf=aitp20210 BACKGROUND Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that. TOPICS - AI, machine learning and big-data methods in theorem proving and mathematics. - Collaboration between automated and interactive theorem proving, in particular their AI/ML aspects. - Common-sense reasoning and reasoning in science, relations to general AI. - Alignment and joint processing of formal, semi-formal, and informal libraries, Formal Abstracts. - Methods for large-scale computer understanding of mathematics and science. - Combinations of linguistic/learning-based and semantic/reasoning methods - Formal verification of AI and machine learning algorithms, explainable AI . SESSIONS There will be several focused sessions on AI for ATP, ITP, mathematics, physics, relations to general AI, Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. Most of the sessions will be scheduled in the afternoons to allow US participants. CONFIRMED (VIRTUAL) PARTICIPANTS/SPEAKERS (TBC) Michael R. Douglas, Stony Brook University Vlad Firoiu, DeepMind Ben Goertzel, SingularityNET Thomas C. Hales, University of Pittsburgh Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Cezary Kaliszyk, University of Innsbruck Peter Koepke, University of Bonn Michael Kinyon, University of Denver Ramana Kumar, DeepMind David McAllester, Toyota Technological Institute at Chicago Tomáš Mikolov, Czech Technical University in Prague Melanie Mitchell, Santa Fe Institute Adam Pease, Articulate Software Stanislas Polu, OpenAI Markus Rabe, Google Research Fabian Ruhle, CERN Stephan Schulz, DHBW Stuttgart David Stanovský, Charles University Martin Suda, Czech Technical University in Prague Josef Urban, Czech Technical University in Prague Robert Veroff, University of New Mexico Yuhuai (Tony) Wu, University of Toronto CONTRIBUTED TALKS We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2020). DATES Submission deadline: May 5, 2021 Author notification: June 20, 2021 Conference registration: TBA Camera-ready versions: TBA Conference: September 5-10, 2021 POST-PROCEEDINGS We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR). PROGRAM COMMITTEE (TBC) Jasmin Christian Blanchette, INRIA Nancy Ulrich Furbach, University of Koblenz Thibault Gauthier, Czech Technical University in Prague Michael R. Douglas (co-chair), Stony Brook University Thomas C. Hales (co-chair), University of Pittsburgh Sean Holden, University of Cambridge Cezary Kaliszyk (co-chair), University of Innsbruck Michael Kinyon, University of Denver Peter Koepke, University of Bonn Konstantin Korovin, The University of Manchester Ramana Kumar (co-chair), DeepMind Stephan Schulz (co-chair), DHBW Stuttgart Geoff Sutcliffe, University of Miami Christian Szegedy, Google Research Josef Urban (co-chair), Czech Technical University in Prague Sarah Winkler, University of Innsbruck Yuhuai (Tony) Wu, University of Toronto LOCATION AND PRICE The conference will take place from September 5 to September 10 2021 online and physically in the CNRS Paul-Langevin Conference Center (https://www.caes.cnrs.fr/sejours/centre-paul-langevin/) located in the mountain village of Aussois in Savoy. Dominated by the "Dent Parrachee", one of the highest peaks of La Vanoise, Aussois is located on a sunny plateau at 1500 m altitude, offering a magnificent panorama of the surrounding mountains and a direct access to the park of La Vanoise in summer and downhill ski slopes or cross country slopes in winter. The total price for accommodation, food and registration for the five days will be around 600 EUR. ARRIVAL/DEPARTURE Aussois is less than 2h from the airports of Lyon, Geneve, Chambery, Annecy, Grenoble and Turin. There are trains and buses from these airports. Aussois is 7km from the Modane TGV station with direct trains from/to Paris. We will organize a bus for the participants from there to Aussois. Further buses to these airports / station can be found at http://www.a
[Hol-info] ARCADE 2021 - Call for Papers
d Plaisted, The University of North Carolina at Chapel Hill, USA Andrei Popescu, Middlesex University London, UK Andrew Reynolds, University of Iowa, USA Philipp Ruemmer, Uppsala University, Sweden Renate A. Schmidt, The University of Manchester, UK Stephan Schulz, DHBW Stuttgart, Germany Martin Suda, Czech Technical University in Prague, Czechia (co-chair) Geoff Sutcliffe, University of Miami, USA Josef Urban, Czech Technical University in Prague, Czechia Christoph Weidenbach, Max Planck Institute for Informatics, Germany Sarah Winkler, Free University of Bozen-Bolzano, Italy (co-chair) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Bill McCune PhD Award in Automated Reasoning
Automated Reasoning is the area of computer science dedicated to applying reasoning in the form of logic to computing systems. The Bill McCune PhD Award in Automated Reasoning distinguishes each year a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. The Bill McCune PhD Award in Automated Reasoning is named after the American computer scientist William Walker McCune. * Eligibility * Eligible for the award are those who successfully defended their PhD - at an academic institution; - in the field of Automated Reasoning; - in the period from January 1, 2020 - December 31, 2020 (for the 2020 award); - in the period from January 1, 2019 - December 31, 2019 (for the 2019 award). The PhD students supervised by the Expert Committee members are not eligible. * Nomination * Candidates for the award must be nominated by their supervisor(s) and one additional independent researcher who reviewed/examined the thesis. Nominations are to be submitted via EasyChair, by March 15, 2021, using the link: https://easychair.org/my/conference?conf=mccuneaward20192020 The nomination must consist of a single PDF file containing - a letter from the supervisor(s) describing why the thesis should be considered for the award and the relationship of the contributions to CADE/IJCAR; - a report from the nominating additional independent researcher who reviewed/examined the thesis; - the thesis itself; - a copy of the PhD diploma; - and copy/copies of CADE/IJCAR papers of the nominee, if any, containing results published in the thesis. The thesis will be evaluated with respect to its quality, originality and (potential) impact to the field of Automated Reasoning. * Procedure * - The nominations will be evaluated and compared by an international Expert Committee (see below). - The procedure to be followed is analogous to the review phase of a conference. The justification by the supervisor and the nominating additional independent researcher report will play an important role in the evaluation. - The final decision is made by the Expert Committee at least one month before CADE/IJCAR being held. - The award consists of a certificate announcing the winner to have received the Bill McCune PhD Award in Automated Reasoning. The award will be announced at the respective year's CADE/IJCAR. The nominators of the winner will also receive a copy of this certificate. - The decision of the Expert Committee is final and binding, and not subject to discussion. * Expert Committee * The Expert Committee is formed by the board of CADE Trustees with the aim to reflect the broad diversity in the area of Automated Reasoning. It is announced with the call for nominations, and thus formed before the call for nominations. The Committee for the Bill McCune PhD Award 2019 and 2020 consists of the following people: - Nikolaj Bjorner, Microsoft - Pascal Fontaine, University of Liege - Carsten Fuhs, Birkbeck, University of London - Cezary Kaliszyk, University of Innsbruck - Claudia Nalon, University of Brasilia - Giles Reger, The University of Manchester - Giselle Reis, CMU-Qatar - Andy Reynolds, The University of Iowa - Uwe Waldmann, MPI for Informatics The Expert Committee can seek additional expertise, even after the submission deadline for nominations. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Conference on Logic and Argumentation - Call for Papers
Fourth International Conference on Logic and Argumentation (CLAR 2021) 20-22 October 2021, Hangzhou, China Hybrid (physical or virtual attendance) https://www.xixilogic.org/events/clar2021/ The 4th International Conference on Logic and Argumentation (CLAR 2021) invites contributions from logic, artificial intelligence, philosophy, computer science, linguistics, law, and other areas studying logic and formal argumentation. CLAR 2021 will be held in Hangzhou, 20-22 October 2021 at Zhejiang University City College. Due to the uncertainties of the epidemiological situation, the conference will be held in a HYBRID format (virtual and physical attendance both accepted), and we encourage physical participation if possible. Papers accepted to CLAR 2021 will be published as Springer LNAI proceedings, and will be available online during the conference. Authors of selected papers will be invited to submit an extended version to a journal special issue after the conference. More information about CLAR 2021 can be found at the conference website: http://www.xixilogic.org/events/clar2021 The CLAR 2021 conference will highlight recent advances in logic and argumentation and foster interaction between these areas within and outside China. Previous conferences can be accessed via: http://www.xixilogic.org/events/clar List of Topics Suggested topics include, but are not limited to the following: * Abstract argumentation * Applications of logic and/or argumentation * Applied logic * Argumentation and game theory * Argumentation and law * Argumentation and linguistics * Argumentation and medical reasoning * Argumentation in AI * Argument mining * Argumentation schemes * BDI logic * Computational argumentation * Deontic logic * Dynamic epistemic logic and belief revision * Formal models for dialog and argumentation * Informal logic * Judgment aggregation * Knowledge representation and reasoning * Logic for game theory * Logic for multi-agent systems * Logic for semantic web * Logic for social network * Mathematical logic * Modal logic * Nonmonotonic logics * Numerical and uncertainty reasoning * Philosophical logic * Pragma-Dialectics * Preference logic * Structured argumentation * Uncertain argumentation Submission Guidelines We invite two types of submissions: full papers (12 - 20 pages) describing original and unpublished work and extended abstracts (5 - 8 pages) of preliminary original work or extended abstracts of already published work (needs to be highlighted along with the title), from either the field of logic or the field of formal argumentation. Additional support material may be included in an appendix, which may be considered or ignored by the program committee. Submissions must be prepared in LaTeX, using the Springer LNCS style: ftp://ftp.springernature.com/cs-proceeding/llncs/llncs2e.zip Submissions not complying with these guidelines will be desk rejected. Papers in PDF format should be submitted via EasyChair: https://easychair.org/conferences/?conf=clar2021 Each submitted paper will be carefully peer-reviewed by a panel of PC members based on originality, significance, technical soundness, clarity of exposition and relevance for the conference. For each accepted paper, at least one author is expected to register and present the paper at the conference. Important Dates Submission: 30 June 2021 Notification: 1 August 2021 Camera-Ready: 15 August 2021 Conference: 20-22 October 2021 PC Chairs Pietro Baroni, University of Brescia Christoph Benzmüller, Freie Universität Berlin Yì N. Wáng, Sun Yat-sen University For general questions or questions regarding the local organizations please send emails to clar2...@xixilogic.org. Questions regarding the program should go to the PC chairs directly. -- Christoph Benzmüller (http://christoph-benzmueller.de) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CADE-28: Call for Tutorials
CADE-28: Call for Tutorials The 28th International Conference on Automated Deduction (CADE-28) Carnegie Mellon University, Pittsburgh, USA. 11-16th July 2021. http://www.cade-28.info CADE will carefully monitor the development of the COVID-19 pandemic, and take guidance from the health authorities, to determine whether CADE-28 will be physical or online or hybrid. CALL FOR TUTORIALS == Tutorial proposals for CADE-28 are solicited. The tutorials will take place before (11th July) and after (16th July) the conference. Tutorials are expected to be either half-day or full-day events, with a theoretical or applied focus, on a topic of interest to CADE-28. Please provide the following information in your application: + Tutorial title. + Names and affiliations of organizers. + Proposed tutorial duration (from half to one day) and the preferred day. + Brief description of the tutorial's goals and topics to be covered. + Whether or not a version of the tutorial has been given previously, and if/how the intended presentation differs. + Short statement regarding plans in case of an online conference. Within reason, CADE will take care of printing and distributing notes for tutorials that would like this service. Important Dates for Tutorials: + Submission deadline: 07 December 2020 + Notification: 18 December 2020 + Tutorials:11 & 16 July 2021 Proposals for tutorials must be submitted to the CADE-28-WTC track via https://easychair.org/conferences/?conf=cade28 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CADE-28 Call for Papers, Workshops, Tutorials, Competitions
CADE-28: Call for Papers, Workshops, Tutorials and Competitions The 28th International Conference on Automated Deduction (CADE-28) Carnegie Mellon University, Pittsburgh, USA. 11-16th July 2021. http://www.cade-28.info CADE will carefully monitor the development of the COVID-19 pandemic, and take guidance from the health authorities, to determine whether CADE-28 will be physical or online or hybrid. CALL FOR PAPERS === CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including logical foundations, theory and principles, applications in and beyond STEM, implementations, and the use/contribution of automated deduction in AI, are solicited. CADE-28 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction. Important Dates + Abstract deadline:15 February 2021 + Submission deadline: 22 February 2021 + Rebuttal phase:2 April2021 + Notification: 19 April2021 + Final version:31 May 2021 + Conference:12-15 July 2021 Submissions can be made in two categories: + Regular papers. Up to 15 pages in LNCS style. Proofs of theoretical results that do not fit in the page limit may be provided in an appendix. Reviewers may consider additional material in appendices, but submissions must be self- contained within the page limit. + Short papers (including system descriptions, user experiences, domain models, etc.) Up to 10 pages in LNCS style. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, originality, significance, correctness, and readability. If software or data is relevant to a paper, a link that provides access to the software/data must be provided to enable reproduction of results. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chairs may solicit further reviews after the rebuttal period. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at http://www.springer.de/comp/lncs/authors.html Papers must be submitted to the CADE-28 track via https://easychair.org/conferences/?conf=cade28 CALL FOR WORKSHOPS == Workshop proposals for CADE-28 are solicited. The workshops will take place before (11th July) and after (16th July) the conference. Both well-established workshops and newer ones are encouraged. Similarly, proposals for workshops with a tight focus on a core automated reasoning specialization, as well as those with a broader, more applied focus, are welcome. Please provide the following information in your application: + Workshop title. + Names and affiliations of organizers. + Proposed workshop duration (from half a day to two days) and preferred day(s). + Brief description of the goals and the scope of the workshop. Why is the workshop relevant to CADE? + Is the workshop new or has it met previously? In the latter case information on previous meetings should be given (e.g., links to the program, number of submissions, number of participants). + What are the plans for publication? + Short statement regarding plans in case of an online conference. CALL FOR TUTORIALS == Tutorial proposals for CADE-28 are solicited. The tutorials will take place before (11th July) and after (16th July) the conference. Tutorials are expected to be either half-day or full-day events, with a theoretical or applied focus, on a topic of interest to CADE-28. Please provide the following information in your application: + Tutorial title. + Names and affiliations of organizers. + Proposed tutorial duration (from half to one day) and the preferred day. + Brief description of the tutorial's goals and topics to be covered. + Whether or not a version of the tutorial has been given previously, and if/how the intended presentation differs. + Short statement regarding plans in case of an online conference. Within reason, CADE will take care of printing and distributing notes for tutorials that would like this service. CALL FOR COMPETITIONS = The CADE ATP System Competition (CASC), which evaluates automated theorem proving systems for classical logics, has become an integral part of the CADE conferences. Further competition proposals are solicited. The goal is to foster the development of automated reasoning systems and applications, in all areas relevant to automated deduction in a broad sense. Please provide the following information in your application: + Competition title. + Names and affiliations of organizers. + Duration and schedule of the competition. + Room/space requirements. + Description of the competition task and the evaluation procedure. +
[Hol-info] CADE-28 Call for Papers, Workshops, Tutorials, and Competitions
CADE-28: Call for Papers, Workshops, Tutorials and Competitions The 28th International Conference on Automated Deduction (CADE-28) Carnegie Mellon University, Pittsburgh, USA. 11-16th July 2021. http://www.cade-28.info CADE will carefully monitor the development of the COVID-19 pandemic, and take guidance from from the health authorities, to determine whether CADE-28 will be physical or online. CALL FOR PAPERS === CADE is the major international forum for presenting research on all aspects of automated deduction. High-quality submissions on the general topic of automated deduction, including logical foundations, theory and principles, applications in and beyond STEM, implementations, and the use/contribution of automated deduction in AI, are solicited. CADE-28 aims to present research that reflects the broad range of interesting and relevant topics in automated deduction. Important Dates + Abstract deadline:15 February 2021 + Submission deadline: 22 February 2021 + Rebuttal phase:2 April2021 + Notification: 19 April2021 + Final version:31 May 2021 Submissions can be made in two categories: + Regular papers. Up to 15 pages in LNCS style. Proofs of theoretical results that do not fit in the page limit may be provided in an appendix. Reviewers may consider additional material in appendices, but submissions must be self- contained within the page limit. + Short papers (including system descriptions, user experiences, domain models, etc.) Up to 10 pages in LNCS style. Submissions must be unpublished and not submitted for publication elsewhere. They will be judged on relevance, originality, significance, correctness, and readability. If software or data is relevant to a paper, a link that provides access to the software/data must be provided to enable reproduction of results. The review process will include a feedback/rebuttal period where authors will have the option to respond to reviewer comments. The PC chairs may solicit further reviews after the rebuttal period. The proceedings of the conference will be published in the Springer LNCS/LNAI series. Formatting instructions and the LNCS style files can be obtained at http://www.springer.de/comp/lncs/authors.html Papers must be submitted to the CADE-28 track via https://easychair.org/conferences/?conf=cade28 CALL FOR WORKSHOPS == Workshop proposals for CADE-28 are solicited. The workshops will take place before the conference. Both well-established workshops and newer ones are encouraged. Similarly, proposals for workshops with a tight focus on a core automated reasoning specialization, as well as those with a broader, more applied focus, are welcome. Please provide the following information in your application document: + Workshop title. + Names and affiliations of organizers. + Proposed workshop duration (from half a day to two days) and preferred day(s). + Brief description of the goals and the scope of the workshop. Why is the workshop relevant to CADE? + Is the workshop new or has it met previously? In the latter case information on previous meetings should be given (e.g., links to the program, number of submissions, number of participants). + What are the plans for publication? + Short statement regarding plans in case of an online conference. CALL FOR TUTORIALS == Tutorial proposals for CADE-28 are solicited. The tutorials will take place before the conference. Tutorials are expected to be either half-day or full-day events, with a theoretical or applied focus, on a topic of interest to CADE-28. Proposals should provide the following information: + Tutorial title. + Names and affiliations of organizers. + Proposed tutorial duration (from half to one day) and the preferred day. + Brief description of the tutorial's goals and topics to be covered. + Whether or not a version of the tutorial has been given previously, and if/how the intended presentation differs. + Short statement regarding plans in case of an online conference. Within reason, CADE will take care of printing and distributing notes for tutorials that would like this service. CALL FOR COMPETITIONS = The CADE ATP System Competition (CASC), which evaluates automated theorem proving systems for classical logics, has become an integral part of the CADE conferences. Further competition proposals are solicited. The goal is to foster the development of automated reasoning systems and applications, in all areas relevant to automated deduction in a broad sense. Proposals should include the following information: + Competition title. + Names and affiliations of organizers. + Duration and schedule of the competition. + Room/space requirements. + Description of the competition task and the evaluation procedure. + Is the competition new or has it been organized before? In the latter case information on previous competitions should be given. +
[Hol-info] CICM 2020 - Call for (free) Participation
= CALL FOR PARTICIPATION CICM 2020 -- Conference on Intelligent Computer Mathematics https://cicm-conference.org/2020/ Due to the Covid-19 outbreak, CICM 2020 is held as an online conference == GENERAL INFORMATION Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. Separate communities have developed to investigate and build computer based systems for computer algebra, automated deduction, and mathematical publishing as well as novel user interfaces. While all of these systems excel in their own right, their integration can lead to synergies offering significant added value. The Conference on Intelligent Computer Mathematics (CICM) offers a venue for discussing and developing solutions to the great challenges posed by the integration of these diverse areas. REGISTRATION -- The conference and the affiliated events will take place online. Registration is free of charge. However, registration is mandatory to attend the talks. Please fill this form to register for CICM 2020. https://forms.gle/oS5BVGDf6LgDGDiK8 SCIENTIFIC PROGRAM The program of the conference is available under: https://easychair.org/smart-program/CICM-13/ (all times are in CEST timezone (UTC+2)) INVITED SPEAKERS - Kevin Buzzard, Imperial College, London, UK Formalizing Undergraduate Mathematics - Catherine Dubois, ENSIIE, CNRS, Evry, France Formally Verified Constraints Solvers: a Guided Tour - Christian Szegedy, Google Research, Mountain View, CA, USA A Promising Path Towards Autoformalization and General Artificial Intelligence INVITED WORKSHOP SPEAKERS --- - Freek Wiedijk, Radboud University Nijmegen, NL Formal Proof for the Future - Fairouz Kamareddine, Heriot-Watt University, UK TBA AFFILIATED WORKSHOPS AND DOCTORAL PROGRAMME --- - NFM 2020 - Workshop on Natural Formal Mathematics (https://cicm-conference.org/2020/cicm.php?event=NFM) - Doctoral Programme (https://cicm-conference.org/2020/cicm.php?event=doctoral) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2020 - Call for Participation
= CALL FOR PARTICIPATION IJCAR 2020 https://ijcar2020.org Co-located with FSCD 2020 (https://fscd-ijcar-2020.org) Due to the Covid-19 outbreak, IJCAR 2020 will be an online conference == GENERAL INFORMATION The International Joint Conference on Automated Reasoning (IJCAR) is the premier international joint conference on all topics in automated reasoning. IJCAR 2020 is the merger of the following leading events in automated reasoning: - CADE (Conference on Automated Deduction) - FroCoS (Symposium on Frontiers of Combining Systems) - ITP (International Conference on Interactive Theorem Proving) - TABLEAUX (Conference on Analytic Tableaux and Related Methods) REGISTRATION -- The conference and the affiliated events will take place online. Registration is free of charge and is mandatory to attend the talks. The registration page is already open and linked from: https://fscd-ijcar-2020.org/register SCIENTIFIC PROGRAM The program of the conference is available under: https://easychair.org/smart-program/IJCAR2020/ (all times are in CEST timezone (UTC+2)) INVITED SPEAKERS - Clark Barrett (https://theory.stanford.edu/~barrett/) - John Harrison (IJCAR-FSCD joint speaker) (https://www.cl.cam.ac.uk/~jrh13/) - Elaine Pimentel (https://www.mat.ufrn.br/~elaine/) - Ruzica Piskac (http://www.cs.yale.edu/homes/piskac/) - René Thiemann (FSCD-IJCAR joint speaker) (http://cl-informatik.uibk.ac.at/users/thiemann/) IJCAR AFFILIATED WORKSHOPS -- - PG: Proof Ground 2020 Interactive Proving Contests https://www21.in.tum.de/~wimmers/proofground/ - LFMTP: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice https://lfmtp.org/workshops/2020/ - Isabelle: Isabelle Workshop https://sketis.net/isabelle/isabelle-workshop-2020 - PAAR: Workshop on Practical Aspects of Automated Reasoning http://paar2020.gforge.inria.fr/ - Coq: The Coq Workshop https://coq-workshop.gitlab.io/2020/ - SMT: International Workshop on Satisfiability Modulo Theories http://smt-workshop.cs.uiowa.edu/2020/index.shtml IJCAR AFFILIATED COMPETITIONS --- - The CADE ATP System Competition CASC-J10 http://www.tptp.org/CASC/J10/ - Termination and Complexity Competition 2020 http://www.termination-portal.org/wiki/Termination_Competition_2020 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CASC-J10 - The CADE ATP System Competition
--- CASC-J10 - The CADE ATP System Competition to be held at The 10th International Joint Conference on Automated Reasoning Online, Earth 29th June -6th July 2020 The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J10 will be held on the 2nd July 2020, during the 10th International Joint Conference on Automated Reasoning. CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of: + the number of problems solved, and + the number of problems solved with a solution output, and + the average runtime for problems solved; in the context of: + a bounded number of eligible problems, chosen from the TPTP library, and + specified time limits for solution attempts. The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. Further details and registration information are available at: http://www.tptp.org/CASC/J10/ Registration of systems for CASC-J10 is now invited. System registration closes on 5th June. Please register early so that adequate resources can be allocated. DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! --- ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Alonzo Church Award - Call for Nominations
Subject: 2020 Alonzo Church Award: Call for Nominations (2) --- CALL FOR NOMINATIONS [REMINDER, DEADLINE SOON] The 2020 Alonzo Church Award for Outstanding Contributions to Logic and Computation INTRODUCTION An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see: https://siglog.acm.org/alonzo-church-award-for-outstanding-contributions-to-logic-and-computation-2020/, https://www.eatcs.org/index.php/church-award/, and https://eacsl.org/. The 2020 Alonzo Church Award was given jointly to Murdoch J. Gabbay and Andrew M. Pitts for their ground-breaking work introducing the theory of nominal representations, see: http://siglog.org/winners-of-the-2019-alonzo-church-award/. Previous awardees are listed at https://www.eatcs.org/index.php/church-award. ELIGIBILITY AND NOMINATIONS The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2020 award, the cut-off date is January 1, 1995. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Gödel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference. Nominations for the 2020 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness. Nominations should be submitted to thomas.ei...@tuwien.ac.at by April 1, 2020. PRESENTATION OF THE AWARD The 2020 award will be presented at CSL 2021, the annual conference of the European Association for Computer Science Logic, which is scheduled to take place in Ljubliana in January 2021. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared. AWARD COMMITTEE The 2020 Alonzo Church Award Committee consists of the following five members: Mariangiola Dezani, Thomas Eiter (chair), Javier Esparza, Radha Jagadeesan, Natarajan Shankar . ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] PAAR 2020 CFP - 7th Workshop on Practical Aspects of Automated Reasoning
** PAAR-2020: 7TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING June 30th, 2020, Paris, France Web site: http://paar2020.gforge.inria.fr/ Submission link: https://easychair.org/conferences/?conf=paar2020 Abstract registration deadline: April 8, 2020 (tentative) Submission deadline: April 15, 2020 (tentative) Topics: automated reasoning, implementation, tools ** The automation of logical reasoning is a challenge that has been studied intensively in fields including mathematics, philosophy, and computer science. PAAR is the workshop on turning this theory into practice: how can automated reasoning tools be built that work and are useful in applications? PAAR covers all aspects of this challenge: which theories, logics, or fragments are well- behaved in practice, and connect well to application domains; which reasoning tasks are tractable and useful; which algorithms are able to solve real-world instances; how should automated reasoning tools be designed, implemented, tested, and evaluated? The goal of PAAR is to bring together theoreticians, tool developers, and users, to concentrate on the practical aspects of automated reasoning. The workshop welcomes high-quality contributions of any kind, including new research results, presentation of work in progress, presentation of new tools, new implementation techniques, new application domains, or case studies. Submission Guidelines - Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages) via EasyChair at https://easychair.org/conferences/?conf=paar2020. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. Submissions should be prepared in LaTeX using the EasyChair proceedings style. The package containing the class file and its user guide and some helper tools can be downloaded from http://www.easychair.org/publications/easychair.zip. Topics include, but are not limited to: -- * automated reasoning in propositional, first-order, higher-order, and non-classical logics; * implementation of provers (SAT, SMT, resolution, superposition, tableau, instantiation-based, rewriting, logical frameworks, etc.); * automated reasoning tools for all kinds of practical problems and applications; * pragmatics of automated reasoning within proof assistants; * practical experiences, usability aspects, feasibility studies; * evaluation of implementation techniques and automated reasoning tools; * performance aspects, benchmarking approaches; non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new applications; * implementation techniques, optimisation techniques, machine learning, strategies and heuristics, fairness; * tools or methods that support prover development; * system descriptions and demos. Programme Committee --- * Simon Cruanes, Aesthetic Integration, Texas, USA * Hans de Nivelle, Nazarbayev University, Kazakhstan * Bruno Dutertre, SRI international, California, USA * Gabriel Ebner, VU Amsterdam, Netherlands * Pascal Fontaine (co-chair), Liège University, Belgium * Antti Hyvärinen, University of Lugano, Switzerland * Ahmed Irfan, Stanford University, California, USA * Cezary Kaliszyk, University of Innsbruck, Austria * Daniel Le Berre, CNRS - University of Artois, France * Ondrej Lengal, Brno University of Technology, Czech Republic * Tomer Libal, American University of Paris, France * Cláudia Nalon, University of BrasÃlia, Brasil * Jens Otten, University of Oslo, Norway * Philipp Ruemmer (co-chair), Uppsala University, Sweden * Renate A. Schmidt, The University of Manchester, UK * Stephan Schulz, DHBW Stuttgart, Germany * Martina Seidl, Johannes Kepler University Linz, Austria * Mihaela Sighireanu, IRIF, University Paris Diderot and CNRS, France * Alexander Steen, University of Luxembourg, Luxembourg * Martin Suda, Czech Technical University, Czech Republic * Geoff Sutcliffe, University of Miami, Florida, USA * Sophie Tourret (co-chair), Max-Planck Institute for Informatics, Germany * Sarah Winkler, University of Verona, Italy * Aleksandar Zeljic, Stanford University, California, USA Publication --- PAAR proceedings will be published electronically in the CEUR workshop proceedings. Venue - Paris, France Important dates --- Abstract registration deadline: April 8
[Hol-info] IWIL-14 at LPAR-23 - Call for Papers
14th International Workshop on the Implementation of Logics http://www.eprover.org/EVENTS/IWIL-2020.html CALL FOR PAPERS Deadline: April 12th, 2020. The 14th International Workshop on the Implementation of Logics will be held on 22nd May 2020, in conjunction with the 23rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, in Alicante, Spain. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: + Propositional logic and decision procedures, including SMT + First-order and higher order logics + Non-classical logics, including modal, temporal, description, non-monotonic reasoning + Formal foundations for efficient implementation of logics + Data structures and algorithms for the efficient representation and processing of logical concepts + Proof/model search organization and heuristics for logical reasoning systems + Data analysis and machine learning approaches to search control + Techniques for proof/model search visualization and analysis + Reasoning with ontologies and other large theories + Implementation of efficient theorem provers and model finders for different logics + System descriptions of logical reasoning systems + Issues of reliability, witness generation, and witness verification + Evaluation and benchmarking of provers and other logic-based systems + I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15 pages) via the EasyChair page for IWIL2020. https://easychair.org/conferences/?conf=iwil2020 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. The proceedings will be published as a volume of Kalpa Publications in Computing. Important Dates: + Submission of papers/abstracts: April 12th, 2020 + Notification of acceptance: April 30th, 2020 + Camera ready versions due: May 15th, 2020 + Workshop: May 22nd, 2020 Program committee (so far - more coming): Konstantin Korovin (Co-Chair)University of Manchester Stephan Schulz (Co-Chair)DHBW Stuttgart Martin Suda (Co-Chair)Czech Technical University in Prague Armin BiereJohannes Kepler University Linz Franz BrausseUniversity of Manchester Pascal FontaineUniversité de Liège, Belgium Thibault GauthierCzech Technical University in Prague John HesterUniversity of Florida Jan JakubuvCzech Technical University Yevgeny KazakovThe University of Ulm Jens OttenUniversity of Oslo Giles RegerUniversity of Manchester Andrew ReynoldsUniversity of Iowa Martina SeidlJohannes Kepler University Linz Alexander SteenUniversity of Luxembourg Geoff SutcliffeUniversity of Miami Josef UrbanCzech Technical University in Prague Petar VukmirovicVrije Universiteit Amsterdam to be completed ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-23 - Call for Workshops and Tutorials
CALL FOR WORKSHOPS AND TUTORIALS LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning 22-27 May, 2020, Alicante, Spain https://easychair.org/smart-program/LPAR23/ Workshop and tutorial proposals for LPAR-23 are solicited. These events will take place on May 22 2020, before the main conference. To apply for a workshop or a tutorial, please contact the workshop chair via martin.s...@cvut.cz and specify: * A title of the event. * Names and affiliations of organisers. * Proposed duration (half day or full). * Brief description of the goals and the scope/the topics to be covered. Why is the tutorial/workshop relevant for LPAR? * Whether or not the tutorial/workshop has been organised previously. * For previously organized workshops, information on previous meetings should be given (e.g., links to the program, number of submissions, number of participants). * For workshops: What are the plans for publication? The deadline for submitting workshop/tutorial proposals: March 1, 2020. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CICM 2020 - Call for Papers
Call for Papers formal papers - informal papers - doctoral programme 13th Conference on Intelligent Computer Mathematics - CICM 2020 - July 26-31, 2020 Bertinoro, Italy http://www.cicm-conference.org/2020 Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration. CICM 2020 Invited Speakers: Kevin Buzzard (Imperial College, London, UK) Catherine Dubois (ENSIIE, CNRS, Evry, France) Christian Szegedy (Google Research, Mountain View, CA, USA) CICM 2020 Programme committee: see https://www.cicm-conference.org/2020/cicm.php?event==pc CICM 2020 invites submissions in all topics relating to intelligent computer mathematics, in particular but not limited to * theorem proving and computer algebra * mathematical knowledge management * digital mathematical libraries CICM appreciates the varying nature of the relevant research in this area and invites submissions of different forms: 1) Formal submissions will be reviewed rigorously and accepted papers will be published in a volume of Springer LNCS: * regular papers (up to 15 pages including references) present novel research results * project and survey papers (up to 15 pages + bibliography) summarize existing results * system and dataset descriptions (up to 5 pages including references) present digital artifacts * system entry (1 page according to the given LaTeX template) provides metadata and a quick overview of a new tool or a new release of an existent tool 2) Informal submissions will be reviewed with a positive bias and selected for presentation based on their relevance for the community. * informal papers may present work-in-progress, project announcements, position statements, etc. * posters and system demos will be presented in parallel in special sessions 3) The doctoral programme provides PhD students with a forum to present early results and receive constructive feedback and mentoring. *** Important Dates *** Formal submissions - Abstract deadline: March 01 - Full paper deadline: March 08 - Reviews sent to authors: April 17 - Rebuttals due: April 21 - Notification of acceptance: April 24 - Camera-ready copies due: May 03 - Conference: July 26-31 Informal submissions and doctoral programme Two separate submission rounds are offered so that some authors can make early travel plans while other authors submit spontaneously. - First round submission deadline: April 15 - Notification of acceptance: May1 - Second round submission deadline: June 15 - Notification of acceptance: July 1 All submissions should be made via easychair at https://easychair.org/conferences/?conf=cicm13 As in previous years, we will publish the CICM 2020 proceedings with Springer LNCS. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-23 - Extended deadlines
** LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning Abstract submission: 18 February, 2020 Paper submission: 22 February, 2020 Author notification: 8 April, 2020 Conference dates: 22-27 May, 2020 Location: Alicante, Spain ** The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 23rd LPAR will be held will be held in Alicante, Spain, 22-27 May 2020. The proceedings will be published by EasyChair Publications, in the EPiC Series in Computing. The volume will be open access and the authors will retain copyright. Submission Guidelines = All papers must be original and not simultaneously submitted to another journal or conference. The following paper categories are welcome: Regular papers describing solid new research results. They can be up to 15 pages long in EasyChair style, including figures but excluding references and appendices (that reviewers are not required to read). Where applicable, regular papers are supported by experimental validation. Experimental and tool papers describing implementations of systems, report experiments with implemented systems, or compare implemented systems. Experimental and tool papers should be supported by a link to the artifact/experimental evaluation available to the reviewers. The length of regular papers is limited to 15 pages in the EasyChair style (excluding the blibliography and appendices). The length of experimental and tool papers is limited to 8 pages in the EasyChair style (excluding the bibliography and appendices). Both types of papers must be electronically submitted in PDF via EasyChair: https://easychair.org/conferences/?conf=lpar23 Authors of accepted papers are required to ensure that at least one of them will be present at the conference. List of Topics == New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: Abduction and interpolation methods Answer set programming Automated reasoning Constraint programming Contextual reasoning Decision procedures Description logics Foundations of security Hardware verification Implementations of logic Inconsistency- and exception tolerant reasoning Interactive theorem proving Knowledge representation and reasoning Logic and computational complexity Logic and databases Logic and games Logic and machine learning Logic and the web Logic and types Logic in artificial intelligence Logic of distributed systems Logic of knowledge and belief Logic programming Logical aspects of concurrency Logical foundations of programming Modal and temporal logics Model checking Non-monotonic reasoning Ontologies and large knowledge bases Paraconsistent logics Probabilistic and fuzzy reasoning Program analysis Rewriting Satisfiability checking Satisfiability modulo theories Software verification Specification using logic Unification theory Program Committee Chairs Elvira Albert, Complutense University of Madrid Laura Kovacs, TU Wien Publication === The LPAR-23 proceedings will be published by EasyChair Publication, in the EasyChair EPiC Series in Computing. Contact === For more details about the conference, venue and organization, see the conference webpage https://easychair.org/smart-program/LPAR23/index.html ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 2020 Alonzo Church Award - Call for Nominations
Subject: 2020 Alonzo Church Award: Call for Nominations CALL FOR NOMINATIONS The 2020 Alonzo Church Award for Outstanding Contributions to Logic and Computation INTRODUCTION An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see: https://siglog.acm.org/alonzo-church-award-for-outstanding-contributions-to-logic-and-computation-2020/, https://www.eatcs.org/index.php/church-award/, and https://eacsl.org/. The 2020 Alonzo Church Award was given jointly to Murdoch J. Gabbay and Andrew M. Pitts for their ground-breaking work introducing the theory of nominal representations, see: http://siglog.org/winners-of-the-2019-alonzo-church-award/. Previous awardees are listed at https://www.eatcs.org/index.php/church-award. ELIGIBILITY AND NOMINATIONS The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2020 award, the cut-off date is January 1, 1995. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Gödel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference. Nominations for the 2020 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness. Nominations should be submitted to thomas.ei...@tuwien.ac.at by April 1, 2020. PRESENTATION OF THE AWARD The 2020 award will be presented at CSL 2021, the annual conference of the European Association for Computer Science Logic, which is scheduled to take place in Athens in January 2021. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared. AWARD COMMITTEE The 2020 Alonzo Church Award Committee consists of the following five members: Mariangiola Dezani, Thomas Eiter (chair), Javier Esparza, Radha Jagadeesan, Natarajan Shankar . ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2020 - Call for Papers
. Such a preliminary report may consist of an extended abstract. Each of these papers should bear the phrase "(short paper)" beneath the title. Accepted submissions in this category will be presented as short talks and published in the main proceedings. There will be no downgrading from regular papers or system descriptions to short papers. All submissions should meet high academic standards; proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. BEST PAPER AWARD IJCAR 2020 will recognize the most outstanding submission with a best paper award at the conference. STUDENT TRAVEL AWARDS Woody Bledsoe Travel Awards will be available to support selected students attending the conference. SPECIAL ISSUE = The authors of a selection of the best IJCAR 2020 papers will be invited to submit an extended version of their paper after the conference, to be published in a special issue of Logical Methods in Computer Science. ORGANIZATION Conference Chair: * Kaustuv Chaudhuri (INRIA, Ecole Polytechnique) Programme Chairs: * Nicolas Peltier (CNRS, LIG, Univ. Grenoble Alpes, Grenoble France), * Viorica Sofronie-Stokkermans (University Koblenz-Landau, Koblenz, Germany) Workshop, Tutorial and Competition Chairs: * Giulio Manzonetto (Université Paris-Nord, France) * Andrew Reynolds (University of Iowa, USA) Programme Committee: * Takahito Aoto (Niigata University, Japan) * Carlos Areces (FaMAF Universidad Nacional de Cordoba, Argentina) * Jeremy Avigad (Carnegie Mellon University, USA) * Franz Baader (TU Dresden, Germany) * Peter Baumgartner (Data 61 and CSIRO, Australia) * Christoph Benzmüller (Freie Universität Berlin, Germany) * Yves Bertot (INRIA, Sophia Antipolis, France) * Armin Biere (Johannes Kepler University Linz, Austria) * Nikolaj Bjorner (Microsoft Research, USA) * Jasmin Blanchette (Vrije Universiteit Amsterdam, Netherlands) * Maria Paola Bonacina (Universita degli Studi di Verona, Italy) * James Brotherston (University College London, UK) * Serenella Cerrito (IBISC, Univ. Evry, Paris Saclay University, France) * Agata Ciabattoni (Vienna University of Technology, Austria) * Koen Claessen (Chalmers University of Technology, Gothenburg, Sweden) * Leonardo de Moura (Microsoft Research, USA) * Stéphane Demri (CNRS, LSV, ENS Paris-Saclay, France) * Gilles Dowek (Inria and ENS Paris-Saclay, France) * Marcelo Finger (University of São Paulo, Brazil) * Pascal Fontaine (Universite de Lorraine, CNRS, Inria, LORIA, France) * Didier Galmiche (Universite de Lorraine - LORIA, France) * Silvio Ghilardi (Universita degli Studi di Milano, Italy) * Martin Giese (Universitetet i Oslo, Norway) * Juergen Giesl (RWTH Aachen University, Germany) * Valentin Goranko (Stockholm University, Sweden) * Rajeev Gore (The Australian National University, Australia) * Stefan Hetzl (Vienna University of Technology, Austria) * Marijn J. H. Heule (The University of Texas at Austin, USA) * Cezary Kaliszyk (University of Innsbruck, Austria) * Deepak Kapur (University of New Mexico, USA) * Laura Kovacs (Vienna University of Technology, Austria) * Andreas Lochbihler (Digital Asset (Switzerland) GmbH) * Christopher Lynch (Clarkson University, USA) * Assia Mahboubi (Inria, France) * Panagiotis Manolios (Northeastern University, USA) * Dale Miller (Inria and LIX/Ecole Polytechnique, France) * Claudia Nalon (University of Brasilia, Brazil) * Tobias Nipkow (Technical University of Munich, Germany) * Albert Oliveras (Universitat Politècnica de Catalunya, Spain) * Jens Otten (University of Oslo, Norway) * Lawrence Paulson (University of Cambridge, UK) * Nicolas Peltier (CNRS, LIG, Univ. Grenoble Alpes, Grenoble France) * Frank Pfenning (Carnegie Mellon University, USA) * Andrei Popescu (Middlesex University London, UK) * Andrew Reynolds (University of Iowa, USA) * Christophe Ringeissen (LORIA-INRIA, France) * Christine Rizkallah (University of New South Wales, Australia) * Katsuhiko Sano (Hokkaido University, Japan) * Renate Schmidt (The University of Manchester, UK) * Stephan Schulz (DHBW Stuttgart, Germany) * Roberto Sebastiani (DISI, University of Trento, Italy) * Viorica Sofronie-Stokkermans (University Koblenz-Landau, Koblenz, Germany) * Matthieu Sozeau (INRIA Paris, France) * Martin Suda (Czech Technical University, Czech Republic) * Geoff Sutcliffe (University of Miami, USA) * Sofiene Tahar (Concordia University, Canada) * Cesare Tinelli (The University of Iowa, USA) * Christian Urban (King's College London, UK) * Josef Urban (Czech Technical University in Prague, Czech Republic) * Uwe Waldmann (Max Planck Institute for Informatics, Germany) * Christoph Weidenbach (Max Planck Institute for Informatics, Germany) ___ hol-info mailing list hol-in
[Hol-info] Artificial Intelligence and Theorem Proving 2020 - Second Call for Papers
SECOND CALL FOR CONTRIBUTIONS Artificial Intelligence and Theorem Proving, AITP 2020 March 22-27, 2020, Aussois, France http://aitp-conference.org/2020 Deadline: December 3, 2019 https://easychair.org/conferences/?conf=aitp2020 BACKGROUND Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the forces driving the progress towards that. TOPICS - AI, machine learning and big-data methods in theorem proving and mathematics. - Collaboration between automated and interactive theorem proving, in particular their AI/ML aspects. - Common-sense reasoning and reasoning in science. - Alignment and joint processing of formal, semi-formal, and informal libraries, Formal Abstracts. - Methods for large-scale computer understanding of mathematics and science. - Combinations of linguistic/learning-based and semantic/reasoning methods - Formal verification of AI and machine learning algorithms, explainable AI. SESSIONS There will be several focused sessions on AI for ATP, ITP and mathematics, Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. CONFIRMED PARTICIPANTS/SPEAKERS (TBC) João Araújo, Universidade Nova de Lisboa Kevin Buzzard, Imperial College London Michael R. Douglas*, Stony Brook University Vlad Firoiu, DeepMind Ben Goertzel, SingularityNET Georges Gonthier, INRIA Thomas C. Hales, University of Pittsburgh John Harrison, Amazon Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Michael Kinyon, University of Denver Joao Marques Silva, ANITI, University of Toulouse David McAllester, Toyota Technological Institute at Chicago Tomáš Mikolov, Facebook AI Research Lawrence C. Paulson, University of Cambridge Alison Pease, University of Dundee J.D. Phillips, Northern Michigan University Markus Rabe, Google Research Stephan Schulz, DHBW Stuttgart Daniel Selsam, Microsoft Research Martin Suda, Czech Technical University in Prague David Stanovský, Charles University in Prague Christian Szegedy, Google Research Robert Veroff, University of New Mexico Petr VojtÄchovský, University of Denver *: To be confirmed. CONTRIBUTED TALKS We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2020). DATES Submission deadline: December 3, 2019 Author notification: January 10, 2020 Conference registration: January 21, 2020 Camera-ready versions: March 1, 2020 Conference: March 22 - 27, 2020 POST-PROCEEDINGS We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR). PROGRAM COMMITTEE (TBC) Jasmin Christian Blanchette, INRIA Nancy Ulrich Furbach, University of Koblenz Thibault Gauthier, Czech Technical University in Prague Thomas C. Hales (co-chair), University of Pittsburgh Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Cezary Kaliszyk (co-chair), University of Innsbruck Michael Kinyon, University of Denver Peter Koepke, University of Bonn Michael Kohlhase, FAU Erlangen-Nürnberg Konstantin Korovin, The University of Manchester Ramana Kumar (co-chair), DeepMind Sarah Loos, Google Research Stephan Schulz (co-chair), DHBW Stuttgart Geoff Sutcliffe, University of Miami Josef Urban (co-chair), Czech Technical University in Prague Sarah Winkler, University of Innsbruck LOCATION AND PRICE The conference will take place from March 22 to March 27 2020 in the CNRS Paul- Langevin Conference Center ... https://www.caes.cnrs.fr/sejours/centre-paul-langevin/ ... located in the mountain village of Aussois in Savoy. Dominated by the "Dent Parrachée", one of the highest peaks of La Vanoise, Aussois is located on a sunny plateau at 1500m altitude, offering a magnificent panorama of the surrounding mountains and a direct access to the downhill ski slopes or cross country slopes in winter. The total price for accommodation, food and registration for the five days will be around 600 EUR. ARRIVAL/DEPARTURE Aussois is less than 2h from the airports of Lyon, Geneve, Chambery, Annecy, Grenoble and Turin. There are trains and buses from these airports. Aussois is 7km from the Modane TGV station with direct trains from/to Paris. We will organize a bus for the participants from there to Aussois. Further buses to these airports/station can be found at http://www.altibus.com/ .
[Hol-info] GCAI 2020 Conference and Doctoral Symposium - Calls for Papers and Participation
6th Global Conference on Artificial Intelligence GCAI 2020, Hangzhou, China, 6-9 April 2020 The 6th Global Conference on Artificial Intelligence (GCAI 2020) will be held in Hangzhou, China, 6-9 April 2020, as part of the Zhejiang Logic for AI Summit (ZjuLogAI 2020). With its special focus theme on "Explainable AI and Responsible AI", the summit intends to promote the interplay between logical approaches and machine learning based approaches in order to make AI more transparent, responsible and accountable. http://www.gcai-2020.info/ (GCAI 2020) http://www.xixilogic.org/zjulogai/ (ZjuLogAI 2020) The first day of GCAI 2020 has been set aside for tutorials and a doctoral symposium. Details are provided below. http://www.xixilogic.org/events/gcai2020/doctoral_symposium/ ** GCAI Submission Guidelines ** GCAI 2020 accepts submissions of two types: - Full paper submissions, which must be original and cannot be submitted simultaneously elsewhere. Full paper submissions must be at most 12 pages long, excluding references. Additional support material may be included in an appendix, which may be considered or ignored by the program committee. - Extended abstract submissions, which report on ongoing or preliminary work, or on work that is central to symbolic reasoning and/or machine/deep learning applied to both software and robotic systems, but that has already been submitted or recently published elsewhere as a full paper (in the case of an already published paper, the full version has to be referenced explicitly). Extended abstract submissions must be at most 4 pages long, excluding references. Both types of submissions must be prepared in LaTeX or Microsoft Word using the EasyChair templates, and uploaded in PDF format. Submissions not complying with these guidelines will be rejected at the discretion of the program committee. Each submission will be reviewed by at least two reviewers. Abstracts are due on 23 November 2019, full papers and extended abstracts are due on 30 November 2019, and decisions will be made by 20 January 2020. Submissions: via EasyChair https://easychair.org/conferences/?conf=gcai2020 Instructions for authors and EasyChair paper templates can be found at https://easychair.org/publications/for_authors List of Topics Submissions in all areas of artificial intelligence are welcome. Suggested topics include, but are not limited to: Foundations + Knowledge representation + Cognitive modeling + Perception + Search + Reasoning and programming + Machine learning + Constraints and uncertainty Architectures + Agents and distributed AI + Intelligent user interfaces + Natural language systems and linguistics + Information retrieval + Case-based reasoning + Hierarchical and deep representations + Affective computing Applications + Aviation and aerospace + Education and tutoring systems + Games and entertainment + Law and machine ethics + Mathematics and the sciences + Medicine and healthcare + Management and manufacturing + World Wide Web + Robotics + Security Implications + Philosophical foundations + Social impact and ethics + Evaluation of AI systems + AI education General Chair **** Geoff Sutcliffe (University of Miami, USA) Program Chairs Grégoire Danoy (University of Luxembourg, Luxembourg) Jun Pang (University of Luxembourg, Luxembourg) Program Committee (to be completed) Jose Julio Alferes, Universidade NOVA de Lisboa, Portugal Serge Autexier, DFKI, Germany Christoph Benzmüller, Freie Universität Berlin, Germany Krysia Broda, Imperial College, UK Matthias R. Brust, University of Luxembourg, Luxembourg Gabriella Cortellessa, CNR-ISTC, National Research Council of Italy, Italy Wolfgang Faber, TU Wien, Austria Germain Forestier, Université de Haute Alsace, France Marco Gavanelli, University of Ferrara, Italy Gianluigi Greco, University of Calabria, Italy Mateja Jamnik, University of Cambridge, UK Juan Luis Jiménez Laredo, Université du Havre Normandie, France Tommi Junttila, Aalto University, Finland Panagiotis Kanellopoulos, University of Patras and CTI "Diophantus", Greece Gabriele Kern-Isberner, Technische Universitaet Dortmund, Germany Gang Li, Deakin University, Australia Sanjiang Li, University of Technology, Sydney, Australia Ines Lynce, INESC-ID/IST, Universidade de Lisboa, Portugal George Metcalfe, University of Bern, Switzerland Angelo Montanari, University of Udine, Italy Till Mossakowski, University of Magdeburg, Germany Apivadee Piyatumrong, National Electronics and Computer Technology Center, Thailand Radu-Emil Precup, Politehnica Uni
[Hol-info] IJCAR 2020 - Call for Papers
hrase "(short paper)" beneath the title. Accepted submissions in this category will be presented as short talks and published in the main proceedings. There will be no downgrading from regular papers or system descriptions to short papers. All submissions should meet high academic standards; proofs of theoretical results that do not fit in the page limit, executables of systems, and input data of experiments should be made available, via a reference to a website or in an appendix of the paper. BEST PAPER AWARD IJCAR 2020 will recognize the most outstanding submission with a best paper award at the conference. STUDENT TRAVEL AWARDS Woody Bledsoe Travel Awards will be available to support selected students attending the conference. SPECIAL ISSUE = The authors of a selection of the best IJCAR 2020 papers will be invited to submit an extended version of their paper after the conference, to be published in a special issue of Logical Methods in Computer Science. ORGANIZATION Conference Chair: * Kaustuv Chaudhuri (INRIA, Ecole Polytechnique) Programme Chairs: * Nicolas Peltier (CNRS, LIG, Univ. Grenoble Alpes, Grenoble France), * Viorica Sofronie-Stokkermans (University Koblenz-Landau, Koblenz, Germany) Workshop, Tutorial and Competition Chairs: * Giulio Manzonetto (Université Paris-Nord, France) * Andrew Reynolds (University of Iowa, USA) Programme Committee: * Takahito Aoto (Niigata University, Japan) * Carlos Areces (FaMAF Universidad Nacional de Cordoba, Argentina) * Jeremy Avigad (Carnegie Mellon University, USA) * Franz Baader (TU Dresden, Germany) * Peter Baumgartner (Data 61 and CSIRO, Australia) * Christoph Benzmüller (Freie Universität Berlin, Germany) * Armin Biere (Johannes Kepler University Linz, Austria) * Nikolaj Bjorner (Microsoft Research, USA) * Jasmin Blanchette (Vrije Universiteit Amsterdam, Netherlands) * Maria Paola Bonacina (Universita degli Studi di Verona, Italy) * James Brotherston (University College London, UK) * Serenella Cerrito (IBISC, Univ. Evry, Paris Saclay University, France) * Agata Ciabattoni (Vienna University of Technology, Austria) * Koen Claessen (Chalmers University of Technology, Gothenburg, Sweden) * Leonardo de Moura (Microsoft Research, USA) * Stéphane Demri (CNRS, LSV, ENS Paris-Saclay, France) * Gilles Dowek (Inria and ENS Paris-Saclay, France) * Marcelo Finger (University of São Paulo, Brazil) * Pascal Fontaine (Universite de Lorraine, CNRS, Inria, LORIA, France) * Didier Galmiche (Universite de Lorraine - LORIA, France) * Silvio Ghilardi (Universita degli Studi di Milano, Italy) * Martin Giese (Universitetet i Oslo, Norway) * Juergen Giesl (RWTH Aachen University, Germany) * Valentin Goranko (Stockholm University, Sweden) * Rajeev Gore (The Australian National University, Australia) * Stefan Hetzl (Vienna University of Technology, Austria) * Marijn J. H. Heule (The University of Texas at Austin, USA) * Cezary Kaliszyk (University of Innsbruck, Austria) * Deepak Kapur (University of New Mexico, USA) * Laura Kovacs (Vienna University of Technology, Austria) * Christopher Lynch (Clarkson University, USA) * Assia Mahboubi (Inria, France) * Panagiotis Manolios (Northeastern University, USA) * Dale Miller (Inria and LIX/Ecole Polytechnique, France) * Claudia Nalon (University of Brasilia, Brazil) * Tobias Nipkow (Technical University of Munich, Germany) * Albert Oliveras (Universitat Politècnica de Catalunya, Spain) * Jens Otten (University of Oslo, Norway) * Lawrence Paulson (University of Cambridge, UK) * Frank Pfenning (Carnegie Mellon University, USA) * Andrei Popescu (Middlesex University London, UK) * Andrew Reynolds (University of Iowa, USA) * Christophe Ringeissen (LORIA-INRIA, France) * Katsuhiko Sano (Hokkaido University, Japan) * Renate Schmidt (The University of Manchester, UK) * Stephan Schulz (DHBW Stuttgart, Germany) * Roberto Sebastiani (DISI, University of Trento, Italy) * Martin Suda (Czech Technical University, Czech Republic) * Geoff Sutcliffe (University of Miami, USA) * Sofiene Tahar (Concordia University, Canada) * Cesare Tinelli (The University of Iowa, USA) * Christian Urban (King's College London, UK) * Josef Urban (Czech Technical University in Prague, Czech Republic) * Uwe Waldmann (Max Planck Institute for Informatics, Germany) * Christoph Weidenbach (Max Planck Institute for Informatics, Germany) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Artificial Intelligence and Theorem Proving 2020 - Call for Papers
CALL FOR CONTRIBUTIONS Artificial Intelligence and Theorem Proving AITP 2020 March 22-27, 2020, Aussois, France http://aitp-conference.org/2020 Deadline: December 3, 2019 https://easychair.org/conferences/?conf=aitp2020 BACKGROUND Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that. TOPICS - AI, machine learning and big-data methods in theorem proving and mathematics. - Collaboration between automated and interactive theorem proving, in particular their AI/ML aspects. - Common-sense reasoning and reasoning in science. - Alignment and joint processing of formal, semi-formal, and informal libraries, Formal Abstracts. - Methods for large-scale computer understanding of mathematics and science. - Combinations of linguistic/learning-based and semantic/reasoning methods - Formal verification of AI and machine learning algorithms, explainable AI . SESSIONS There will be several focused sessions on AI for ATP, ITP and mathematics, Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. CONFIRMED PARTICIPANTS/SPEAKERS (TBC) João Araújo, Universidade Nova de Lisboa Kevin Buzzard, Imperial College London Michael R. Douglas*, Stony Brook University Vlad Firoiu, DeepMind Ben Goertzel, SingularityNET Georges Gonthier, INRIA Thomas C. Hales, University of Pittsburgh John Harrison, Amazon Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Michael Kinyon, University of Denver Joao Marques Silva, ANITI, University of Toulouse David McAllester, Toyota Technological Institute at Chicago Tomáš Mikolov, Facebook AI Research Lawrence C. Paulson, University of Cambridge Alison Pease, University of Dundee Markus Rabe, Google Research Stephan Schulz, DHBW Stuttgart Daniel Selsam, Microsoft Research Martin Suda, Czech Technical University in Prague Robert Veroff, University of New Mexico Petr Vojtchovsky, University of Denver *: To be confirmed. CONTRIBUTED TALKS We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2020). DATES Submission deadline: December 3, 2019 Author notification: January 10, 2020 Conference registration: January 21, 2020 Camera-ready versions: March 1, 2020 Conference: March 22 - 27, 2020 POST-PROCEEDINGS We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR). PROGRAM COMMITTEE (TBC) Jasmin Christian Blanchette, INRIA Nancy Ulrich Furbach, University of Koblenz Tibault Gauthier, Czech Technical University in Prague Thomas C. Hales (co-chair), University of Pittsburgh Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Cezary Kaliszyk (co-chair), University of Innsbruck Peter Koepke, University of Bonn Konstantin Korovin, The University of Manchester Ramana Kumar (co-chair), DeepMind Sarah Loos, Google Research Stephan Schulz (co-chair), DHBW Stuttgart Geoff Sutcliffe, University of Miami Josef Urban (co-chair), Czech Technical University in Prague Sarah Winkler, University of Innsbruck LOCATION AND PRICE The conference will take place from March 22 to March 27 2020 in the CNRS Paul-Langevin Conference Center (https://www.caes.cnrs.fr/sejours/centre-paul-langevin/) located in the mountain village of Aussois in Savoy. Dominated by the "Dent Parrachee", one of the highest peaks of La Vanoise, Aussois is located on a sunny plateau at 1500 m altitude, offering a magnificent panorama of the surrounding mountains and a direct access to the downhill ski slopes or cross country slopes in winter. The total price for accommodation, food and registration for the five days will be around 600 EUR. ARRIVAL/DEPARTURE Aussois is less than 2h from the airports of Lyon, Geneve, Chambery, Annecy, Grenoble and Turin. There are trains and buses from these airports. Aussois is 7km from the Modane TGV station with direct trains from/to Paris. We will organize a bus for the participants from there to Aussois. Further buses to these airports/station can be found at http://www.altibus.com/ . ORGANIZERS Cezary Kaliszyk and Josef Urban ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] TPTP v7.3.0 released
The TPTP Problem Library, Release v7.3.0 Geoff Sutcliffe Dep't of Computer Science, University of Miami, USA ge...@cs.miami.edu *** NOTICE: The CADE-27 ATP System Competition (CASC-27) will run on Wednesday. *** See the action online at ... ***http://www.tptp.org/CASC/27/ The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems. The TPTP supplies the ATP community with: + A comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism. + A comprehensive list of references and other interesting information for each problem. + Arbitary size instances of generic problems (e.g., the N-queens problem). + A utility to convert the problems to existing ATP systems' formats. + General guidelines outlining the requirements for ATP system evaluation. + Standards for input and output for ATP systems. The principal motivation for the TPTP is to support the testing and evaluation of ATP systems, to help ensure that performance results accurately reflect capabilities of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library. This is the first release with polymorphic THF (TH1) problems. There are 644 polymorphic TH1 problems in 14 domains. TPTP v7.3.0 is now available at: http://www.tptp.org The TPTP-v7.3.0.tgz file contains the library, including utilities and basic documentation. Full documentation is online at: http://www.tptp.org/TPTP/TR/TPTPTR.shtml The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user, and be kept informed of such developments, please email Geoff Sutcliffe. == What's New in TPTP v7.3.0 == Release v7.3.0, Fri Aug 2 16:17:10 EDT 2019 Changes from v7.2.0 to v7.3.0 for THF problems 8 bugfixes done, in the domains LCL. Changes from v7.2.0 to v7.3.0 for TFA problems 6 new abstract problems, in the domains PLA. 7 new problems, in the domains PLA. Changes from v7.2.0 to v7.3.0 for FOF problems 286 new abstract problems, in the domains CSR NUN SEV SWW. 458 new problems, in the domains CSR NUM NUN SEV SWW. 247 bugfixes done, in the domains CSR NUN SET. Changes from v7.2.0 to v7.3.0 for CNF problems 45 new abstract problems, in the domains SYO. 196 new problems, in the domains AGT ALG ANA BOO CAT COL CSR GRP HEN KLE LAT LCL MSC NLP NUM PLA PUZ REL RNG ROB SEU SWB SWV SYN SYO. 16 bugfixes done, in the domains SET. + In SyntaxBNF - Added semantic rules for . - Split into and , and added () to . ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] GCAI 2020, Hangzhou, China - Call for Papers
6th Global Conference on Artificial Intelligence GCAI 2020, Hangzhou, China, 6-9 April 2020 http://www.gcai-2020.info/ The 6th Global Conference on Artificial Intelligence (GCAI 2020) will be held in Hangzhou, China, 6-9 April 2020, as part of the Zhejiang Logic for AI Summit (ZjuLogAI 2020). With its special focus theme on "Explainable AI and Responsible AI", the summit intends to promote the interplay between logical approaches and machine learning based approaches in order to make AI more transparent, responsible and accountable. http://www.gcai-2020.info/ (GCAI 2020) http://www.xixilogic.org/zjulogai/ (ZjuLogAI 2020) Submission Guidelines GCAI 2020 accepts submissions of two types: - Full paper submissions, which must be original and cannot be submitted simultaneously elsewhere. Full paper submissions must be at most 12 pages long, excluding references. Additional support material may be included in an appendix, which may be considered or ignored by the program committee. - Extended abstract submissions, which report on ongoing or preliminary work, or on work that is central to symbolic reasoning and/or machine/deep learning applied to both software and robotic systems, but that has already been submitted or recently published elsewhere as a full paper (in the case of an already published paper, the full version has to be referenced explicitly). Extended abstract submissions must be at most 4 pages long, excluding references. Both types of submissions must be prepared in LaTeX or Microsoft Word using the EasyChair templates, and uploaded in PDF format. Submissions not complying with these guidelines will be rejected at the discretion of the program committee. Each submission will be reviewed by at least two reviewers. Abstracts are due on 23 November 2019, full papers and extended abstracts are due on 30 November 2019, and decisions will be made by 20 January 2020. Submissions: via EasyChair https://easychair.org/conferences/?conf=gcai2020 Instructions for authors and EasyChair paper templates can be found at https://easychair.org/publications/for_authors List of Topics Submissions in all areas of artificial intelligence are welcome. Suggested topics include, but are not limited to: Foundations + Knowledge representation + Cognitive modeling + Perception + Search + Reasoning and programming + Machine learning + Constraints and uncertainty Architectures + Agents and distributed AI + Intelligent user interfaces + Natural language systems and linguistics + Information retrieval + Case-based reasoning + Hierarchical and deep representations + Affective computing Applications + Aviation and aerospace + Education and tutoring systems + Games and entertainment + Law and machine ethics + Mathematics and the sciences + Medicine and healthcare + Management and manufacturing + World Wide Web + Robotics + Security Implications + Philosophical foundations + Social impact and ethics + Evaluation of AI systems + AI education General Chair **** Geoff Sutcliffe (University of Miami, USA) Program Chairs Grégoire Danoy (University of Luxembourg, Luxembourg) Jun Pang (University of Luxembourg, Luxembourg) Program Committee The PC members are currently being invited; we plan to have about 50 PC members. Steering Committee Nikolaj Bjorner (Microsoft Research, USA) Adel Bouhoula (University of Carthage, Tunisia) Laura Kovács (Chalmers University, Sweden) Sriram Rajamani (Microsoft Research, India) Geoff Sutcliffe (University of Miami, USA) Andrei Voronkov (University of Manchester, UK) Organizing Committee Organizing Committee of ZjuLogAI can be found at http://www.xixilogic.org/zjulogai/ Publication GCAI 2020 proceedings will be published in the EasyChair EPiC series in Computing. Proceedings of the previous GCAI conferences are available online: Georg Gottlob, Geoff Sutcliffe and Andrei Voronkov (editors). GCAI 2015. Global Conference on Artificial Intelligence (EPiC Series in Computing, Volume 36) https://easychair.org/publications/volume/GCAI_2015 Christoph Benzmüller, Geoff Sutcliffe and Raul Rojas (editors). GCAI 2016. 2nd Global Conference on Artificial Intelligence (EPiC Series in Computing, Volume 41) https://easychair.org/publications/volume/GCAI_2016 Christoph Benzmüller, Christine Lisetti and Martin Theobald (editors). GCAI 2017. 3rd Global Conference on Artificial Intelligence (EPiC Series in Computing, Volume 50) https://easychair.org/publications/volume/GCAI_20
[Hol-info] FroCoS-12 and TABLEAUX-28, London, September 2-6. Second call for participation (early registration closes on August 21)
The 2019 editions of FroCoS (the 12th International Symposium on Frontiers of Combining Systems) and TABLEAUX (the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), as well as their affiliated workshops and tutorials, will take place in London, at Middlesex University, on the week of September 2-6. This year we have an exciting program of contributed and invited talks, and affiliated events. Please see https://tableaux2019.org/Program_FroCoS_TABLEAUX_2019.pdf for detailed program information. Moreover, information on traveling and accommodation (including affordable accommodation for budget-constrained participants), and on the sites and activities that can be enjoyed in the Middlesex University's beautiful campus, is available from the conferences' websites: https://frocos2019.org and https://tableaux2019.org Information on registration and fees is also available from these websites. The deadline for early registration is August 21st, 2019. INVITED TALKS * Jeremy Avigad. Automated Reasoning for the Working Mathematician * Maria Paola Bonacina. Conflict-Driven Reasoning in Unions of Theories * Stephane Graham-Lengrand. Recent and Ongoing Developments of Model-Constructing Satisfiability * Stephane Graham-Lengrand and Sara Negri. Remembering Roy Dyckhoff * Uli Sattler. Modularity and Automated Reasoning in Description Logics AFFILIATED WORKSHOPS * The 25th Workshop on Automated Reasoning (ARW 2019), organized by Alexander Bolotov and Florian Kammueller * Journeys in Computational Logic: Tributes to Roy Dyckhoff, organized by Stephane Graham-Lengrand, Ekaterina Komendantskaya and Mehrnoosh Sadrzadeh AFFILIATED TUTORIALS * Formalising Concurrent Computation: CLF, Celf, and Applications by Sonia Marin * How to Build an Automated Theorem Prover -- An Introductory Tutorial (invited TABLEAUX tutorial) by Jens Otten For any questions, please contact the organizers at ch...@tableaux2019.org or ch...@frocos2019.org. We hope to see many of you this September in London. Best wishes, Serenella Cerrito, Andreas Herzig, Andrei Popescu and Franco Raimondi (program chairs and local organizers) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] FroCoS-12 and TABLEAUX-28
The 2019 editions of FroCoS (the 12th International Symposium on Frontiers of Combining Systems) and TABLEAUX (the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), as well as their affiliated workshops and tutorials will take place in London, at Middlesex University, in the week of September 2-6. This year we have an exciting program of contributed and invited talks, and affiliated events. Please see https://tableaux2019.org/Program_FroCoS_TABLEAUX_2019.pdf for detailed program information. Moreover, information on traveling and accommodation (including affordable accommodation for budget-constrained participants), and on the sites and activities that can be enjoyed in the Middlesex University's beautiful campus, is available from the conferences' websites: https://frocos2019.org and https://tableaux2019.org Information on registration and fees is also available from these websites. The deadline for early registration is August 21st, 2019. INVITED TALKS * Jeremy Avigad. Automated Reasoning for the Working Mathematician * Maria Paola Bonacina. Conflict-Driven Reasoning in Unions of Theories * Stephane Graham-Lengrand. Recent and Ongoing Developments of Model-Constructing Satisfiability * Stephane Graham-Lengrand and Sara Negri. Remembering Roy Dyckhoff * Uli Sattler. Modularity and Automated Reasoning in Description Logics AFFILIATED WORKSHPS * The 25th Workshop on Automated Reasoning (ARW 2019), organized by Alexander Bolotov and Florian Kammueller * Journeys in Computational Logic: Tributes to Roy Dyckhoff, organized by Stephane Graham-Lengrand, Ekaterina Komendantskaya and Mehrnoosh Sadrzadeh AFFILIATED TUTORIALS * Formalising Concurrent Computation: CLF, Celf, and Applications by Sonia Marin, Giselle Reis and Iliano Cervesato * How to Build an Automated Theorem Prover---An Introductory Tutorial (invited TABLEAUX tutorial) by Jens Otten. For any questions, please contact the organizers at ch...@tableaux2019.org or ch...@frocos2019.org. We hope to see many of you this September in London. Best wishes, Serenella Cerrito, Andreas Herzig, Andrei Popescu and Franco Raimondi (program chairs and local organizers) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] ARCADE 2019 - submission deadline extension
The submission deadline of ARCADE 2019 has been extended to 23 June 2019! ARCADE is a lively informal workshop, intended to discuss ideas, challenges and directions related to the future of automated reasoning. Make it more interesting and fun by contributing your ideas! *** CALL FOR PAPERS *** ARCADE http://arcade2019.net/ Automated Reasoning: Challenges, Applications, Directions, Exemplary achievements 26 August 2019, Natal, Brazil (co-located with CADE-27) DESCRIPTION: The main goal of this workshop is to bring together key people from various subcommunities of automated reasoning---such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving---to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community. The structure of the workshop will be informal. We invite extended abstracts (2-4 pages, using the EasyChair class style http://www.easychair.org/publications/for_authors) in the form of non-technical position statements aimed at prompting lively discussion. The title of the workshop is indicative of the kind of discussions we would like to encourage: Challenges: What are the next grand challenges for research on automated reasoning? Thereby, we refer to problems, solving which would imply a significant impact (e.g., shift of focus) on the CADE community and beyond. Applications: Where is automated reasoning applicable in real-world (industrial) scenarios? Which directions should be pursued to open new application domains? Directions: Based on the grand challenges and requirements from real-world applications, what are the research directions the community should promote? What bridges between the different subcommunities of automated reasoning need to be strengthened? What new communities should be included (if at all)? Exemplary achievements: What are the landmark achievements of automated reasoning whose influence reached far beyond the CADE community itself? What can we learn from those successes when shaping our future research? Input from our community raised exciting questions like the following: - What is the role of automated reasoning in AI, and vice versa? - How can AR help to obtain explainable AI? - What can full first-order logic as opposed to SAT/SMT do for verification? - How to identify relevant facts from large knowledge bases? - How can provers exploit semantic knowledge? - How can we ensure reliability of formal verification tools? - How can we attract young people to our field? in addition to many other intriguing issues (see http://arcade2019.net/#topics for an extensive collection). But we are most interested in your take on the upcoming challenges! At the event, contributions will be grouped into similar themes and authors will be invited to make their case within discussion panels. After the workshop, they will be welcome to extend their abstracts for inclusion in an EPiC post-proceedings, taking into account the discussion. Submissions are to be made via the following EasyChair link: https://easychair.org/conferences/?conf=3Darcade2019 IMPORTANT DATES (Anywhere on Earth): New submission deadline: 23 June 2019 New notification: 7 July 2019 Workshop: 26 August 2019 Post-proceedings deadline: 29 September 2019 PROGRAM COMMITTEE: Franz Baader, TU Dresden Christoph Benzmueller, Freie Universitaet Berlin Armin Biere, Johannes Kepler University Linz Nikolaj Bjorner, Microsoft Research Jasmin Christian Blanchette, Inria Nancy & LORIA Maria Paola Bonacina, Universite degli Studi di Verona Pascal Fontaine, LORIA, Inria, University of Lorraine Silvio Ghilardi, Universite degli Studi di Milano Jurgen Giesl, RWTH Aachen Alberto Griggio, FBK-IRST Reiner Hahnle,TU Darmstadt Marijn Heule, The University of Texas at Austin Cezary Kaliszyk, University of Innsbruck Laura Kovacs, Vienna University of Technology Aart Middeldorp, University of Innsbruck Neil Murray, SUNY at Albany David Plaisted, University of North Carolina at Chapel Hill Andrei Popescu, Middlesex University London Renate Schmidt, The University of Manchester Stephan Schulz, DHBW Stuttgart Martin Suda, Czech Technical University (co-chair) Geoff Sutcliffe, University of Miami Josef Urban, Czech Technical University Christoph Weidenbach, Max Planck Institute for Informatics Sarah Winkler, University of Innsbruck (co-chair) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] The 6th Vampire Workshop - CFP
= Vampire 2019: The 6th Vampire Workshop July 7, 2019, affiliated with SAT 2019 Lisboa, Portugal https://easychair.org/smart-program/Vampire2019/index.html = CALL FOR PAPERS = IMPORTANT DATES: - Submission deadline: June 16, 2019 - Notification of acceptance: June 19, 2019 - Workshop day: July 7, 2019 WORKSHOP AIM: The workshop aims at discussing the development and use of the first-order theorem prover Vampire. The workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas. Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The developers can learn more about the use of Vampire, its efficiency in various application areas and needs of the users. The workshop is going to to shed the light on on problems such as - what is essential for substantial progress in theorem proving tools; - what are the best implementation principles to be used; - what are the best heuristics and strategies, depending on application areas; - both successful and unsuccessful case studies; - missing features in modern theorem provers. The workshop will also overview the most recent advances made in Vampire. PAPER SUBMISSION: We seek submissions reporting on theory, application, case studies, experiments and work-in-progress using Vampire and other theorem provers in various applications. Submissions can be in any form, ranging from work in progress to completed work. For example, the users can submit: - extended abstracts or full papers; - theoretical papers; - experimental papers and case studies - or in general any papers that can benefit tool developers and users. Papers can be of any length, ranging from 1-page abstracts to full papers up to 20 pages in length. The papers should use the EasyChair LaTeX, Microsoft Word, or ODT templates, which can be found at: http://www.easychair.org/publications/epic-templates. Submissions should be made using EasyChair, via the link : https://easychair.org/conferences/?conf=vampire2019 The workshop proceedings is planned to be published in the EasyChair EPiC series. PROGRAM CHAIRS: Laura Kovacs (Vienna University of Technology) Andrei Voronkov (University of Manchester and EasyChair) -- ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 6th International Workshop on Proof eXchange for Theorem Proving (PxTP)
Dates * Abstract submission: May 12, 2019 * Paper submission: May 19, 2019 * Notification: June 21, 2019 * Camera ready versions due: July 14, 2019 * Workshop: 25-26 August 2019 ## Invited Speakers TBA ## Program Committee * Haniel Barbosa (University of Iowa), co-chair * Giselle Reis (Carnegie Mellon University), co-chair * Roberto Blanco, Inria, France * Frédéric Blanqui, Inria, France * Simon Cruanes, Aesthetic Integration, USA * Catherine Dubois, ENSIIE, France * Amy Felty, University of Ottawa, Canada * Mathias Fleury, Max-Planck-Institut für Informatik, Germany * Stéphane Graham-Lengrand, SRI, USA * Cezary Kaliszyk, University of Innsbruck, Austria * Chantal Keller, LRI, Université Paris-Sud, France * Laura Kovács, TU Wien, Austria * Olivier Laurent, CNRS, ENS Lyon, France * Stefan Mitsch, Carnegie Mellon University, USA * Carlos Olarte, UFRN, Brazil * Bruno Woltzenlogel Paleo, IOHK, Australia * Florian Rabe, LRI, Université Paris-Sud, France * Martin Riener, University of Manchester, UK * Geoff Sutcliffe, University of Miami, USA * Josef Urban, Czech Institute of Informatics, Robotics and Cybernetics (CIIRC), Czech Republic * Yoni Zohar, Stanford University, USA ## Previous PxTP Editions * PxTP 2017 (https://pxtp.github.io/2017/), affiliated to Tableaux 2017, FroCoS 2017 and ITP 2017 * PxTP 2015 (http://pxtp15.lri.fr/), affiliated to CADE-25 * PxTP 2013 (http://www.cs.ru.nl/pxtp13/), affiliated to CADE-24 * PxTP 2012 (http://pxtp2012.inria.fr/), affiliated to IJCAR 2012 * PxTP 2011 (http://pxtp2011.loria.fr/), affiliated to CADE-23 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Verification Mentoring Workshop 2019: Scholarships
Verification Mentoring Workshop 2019: Call for scholarship applications Verification Mentoring Workshop (VMW 2019) http://i-cav.org/2019/mentoring/ co-located with CAV 2019 13 July 2019 New York City, USA APPLICATIONS FOR TRAVEL SCHOLARSHIPS We warmly invite eligible students to apply for travel scholarships to attend the Verification Mentoring Workshop and CAV. The deadline for applications is April 30. Applications are received via the form at https://forms.gle/6z6kUGPWqGoQ7cka6 ABOUT VMW The purpose of the Verification Mentoring Workshop is to provide mentoring and career advice to early-stage graduate students, to attract them to pursue research careers in the area of computer-aided verification. The workshop will particularly encourage participation of women and underrepresented minorities. The workshop program will include a number of talks and interactive sessions. The talks will give an overview of the field along with brief introductions to the varied topics highlighted at CAV 2019. Other talks will provide mentoring and career advice, from academia and industry. More information can be found at http://i-cav.org/2019/mentoring/ SPEAKERS Aws Albarghouthi, University of Wisconsin-Madison Azadeh Farzan, University of Toronto Vijay Ganesh, University of Waterloo Ranjit Jhala, University of California, San Diego Ruzica Piskac, Yale University Manu Sridharan, University of California, Riverside In case of questions, please contact the organizers Loris D'Antoni (chair) Rayna Dimitrova Cezara Dragoi Anthony W. Lin ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] ARCADE 2019 CFP
*** CALL FOR PAPERS *** ARCADE http://arcade2019.net/ Automated Reasoning: Challenges, Applications, Directions, Exemplary achievements 25 or 26 August 2019, Natal, Brazil (co-located with CADE-27) DESCRIPTION: The main goal of this workshop is to bring together key people from various subcommunities of automated reasoning---such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving---to discuss the present, past, and future of the field. The intention is to provide an opportunity to discuss broad issues facing the community. The structure of the workshop will be informal. We invite extended abstracts (2-4 pages, using the EasyChair class style http://www.easychair.org/publications/for_authors) in the form of non-technical position statements aimed at prompting lively discussion. The title of the workshop is indicative of the kind of discussions we would like to encourage: Challenges: What are the next grand challenges for research on automated reasoning? Thereby, we refer to problems, solving which would imply a significant impact (e.g., shift of focus) on the CADE community and beyond. Applications: Where is automated reasoning applicable in real-world (industrial) scenarios? Which directions should be pursued to open new application domains? Directions: Based on the grand challenges and requirements from real-world applications, what are the research directions the community should promote? What bridges between the different subcommunities of automated reasoning need to be strengthened? What new communities should be included (if at all)? Exemplary achievements: What are the landmark achievements of automated reasoning whose influence reached far beyond the CADE community itself? What can we learn from those successes when shaping our future research? Input from our community raised exciting questions like the following: - What is the role of automated reasoning in AI, and vice versa? - How can AR help to obtain explainable AI? - What can full first-order logic as opposed to SAT/SMT do for verification? - How to identify relevant facts from large knowledge bases? - How can provers exploit semantic knowledge? - How can we ensure reliability of formal verification tools? - How can we attract young people to our field? in addition to many other intriguing issues (see http://arcade2019.net/#topics for an extensive collection). But we are most interested in your take on the upcoming challenges! At the event, contributions will be grouped into similar themes and authors will be invited to make their case within discussion panels. After the workshop, they will be welcome to extend their abstracts for inclusion in an EPiC post-proceedings, taking into account the discussion. Submissions are to be made via the following EasyChair link: https://easychair.org/conferences/?conf=3Darcade2019 IMPORTANT DATES (Anywhere on Earth): Submission deadline: 2 June 2019 Notification: 30 June 2019 Workshop: 26 August 2019 Post-proceedings deadline: 29 September 2019 PROGRAM COMMITTEE: Franz Baader, TU Dresden Christoph Benzmueller, Freie Universitaet Berlin Armin Biere, Johannes Kepler University Linz Nikolaj Bjorner, Microsoft Research Jasmin Christian Blanchette, Inria Nancy & LORIA Maria Paola Bonacina, Universite degli Studi di Verona Pascal Fontaine, LORIA, Inria, University of Lorraine Silvio Ghilardi, Universite degli Studi di Milano Jurgen Giesl, RWTH Aachen Alberto Griggio, FBK-IRST Reiner Hahnle,TU Darmstadt Marijn Heule, The University of Texas at Austin Cezary Kaliszyk, University of Innsbruck Laura Kovacs, Vienna University of Technology Aart Middeldorp, University of Innsbruck Neil Murray, SUNY at Albany David Plaisted, University of North Carolina at Chapel Hill Andrei Popescu, Middlesex University London Renate Schmidt, The University of Manchester Stephan Schulz, DHBW Stuttgart Martin Suda, Czech Technical University (co-chair) Geoff Sutcliffe, University of Miami Josef Urban, Czech Technical University Christoph Weidenbach, Max Planck Institute for Informatics Sarah Winkler, University of Innsbruck (co-chair) ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 6th Workshop on Proof eXchange for Theorem Proving (PxTP) - CFP
: May 12, 2019 * Paper submission: May 19, 2019 * Notification: June 21, 2019 * Camera ready versions due: July 14, 2019 * Workshop: 25-26 August 2019 ## Invited Speakers TBA ## Program Committee * Haniel Barbosa (University of Iowa), co-chair * Giselle Reis (Carnegie Mellon University), co-chair * Roberto Blanco, Inria, France * Frédéric Blanqui, Inria, France * Simon Cruanes, Aesthetic Integration, USA * Catherine Dubois, ENSIIE, France * Amy Felty, University of Ottawa, Canada * Mathias Fleury, Max-Planck-Institut für Informatik, Germany * Stéphane Graham-Lengrand, SRI, USA * Cezary Kaliszyk, University of Innsbruck, Austria * Chantal Keller, LRI, Université Paris-Sud, France * Laura Kovács, TU Wien, Austria * Olivier Laurent, CNRS, ENS Lyon, France * Stefan Mitsch, Carnegie Mellon University, USA * Carlos Olarte, UFRN, Brazil * Bruno Woltzenlogel Paleo, IOHK, Australia * Florian Rabe, LRI, Université Paris-Sud, France * Martin Riener, University of Manchester, UK * Geoff Sutcliffe, University of Miami, USA * Josef Urban, Czech Institute of Informatics, Robotics and Cybernetics (CIIRC), Czech Republic * Yoni Zohar, Stanford University, USA ## Previous PxTP Editions * PxTP 2017 (https://pxtp.github.io/2017/), affiliated to Tableaux 2017, FroCoS 2017 and ITP 2017 * PxTP 2015 (http://pxtp15.lri.fr/), affiliated to CADE-25 * PxTP 2013 (http://www.cs.ru.nl/pxtp13/), affiliated to CADE-24 * PxTP 2012 (http://pxtp2012.inria.fr/), affiliated to IJCAR 2012 * PxTP 2011 (http://pxtp2011.loria.fr/), affiliated to CADE-23 ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 5th Workshop on Bridging the Gap between Human and Automated Reasoning
CALL FOR PAPERS [Apologies if you receive multiple copies of this announcement] [Please kindly help forward it to potentially interested attendees] Fifth Workshop on: Bridging the Gap between Human and Automated Reasoning an IJCAI-19 workshop (supported by IFIP TC12) Macau, China August, 2019 http://ratiolog.uni-koblenz.de/bridging2019 = Reasoning is a core ability in human cognition. Its power lies in the ability to theorize about the environment, to make implicit knowledge explicit, to generalize given knowledge and to gain new insights. There are a lot of findings in cognitive science research which are based on experimental data about reasoning tasks, among others models for the Wason selection task or the suppression task discussed by Byrne and others. This research is supported also by brain researchers, who aim at localizing reasoning processes within the brain. Early work often used propositional logic as a normative framework. Any deviation from it has been considered an error. Central results like findings from the Wason selection task or the suppression task inspired a shift from propositional logic and the assumption of monotonicity in human reasoning towards other reasoning approaches. This includes but is not limited to models using probabilistic approaches, mental models, or non-monotonic logics. Considering cognitive theories for syllogistic reasoning show that none of the existing theories is close to the existing data. But some formally inspired cognitive complexity measures can predict human reasoning difficulty for instance in spatial relational reasoning. Automated deduction, on the other hand, is mainly focusing on the automated proof search in logical calculi. And indeed there is tremendous success during the last decades. Recently a coupling of the areas of cognitive science and automated reasoning is addressed in several approaches. For example there is increasing interest in modeling human reasoning within automated reasoning systems including modeling with answer set programming, deontic logic or abductive logic programming. There are also various approaches within AI research for commonsense reasoning and in the meantime there even exist benchmarks for commonsense reasoning, like the Winograd and the COPA challenge. A core goal of Bridging-the-gap-Workshops is to make results from psychology, cognitive science, and AI accessible to each other. The goal is to develop systems that can adapt themselves to an individuals' reasoning process and that such systems follow the principle of explainable AI to ensure trustfulness and to support the integration of results from other fields. We propose a human syllogistic reasoning challenge to predict future inferences of an individual reasoner based on some previous observations. Hence, participants can develop cognitive AI models (written in Python) that predict the next inference. These predictions are then evaluated in the CCobra framework (for more information see https://www.cognitive-computation.uni-freiburg.de/modelingchallenge). Despite a common research interest -- reasoning -- there are still several milestones necessary to foster a better inter-disciplinary research. First, to develop a better understanding of methods, techniques, and approaches applied in both research fields. Second, to have a synopsis of the relevant state-of-the-art in both research directions. Third, to combine methods and techniques from both fields and find synergies. E.g., techniques and methods from computational logic have never been directly applied to model adequately human reasoning. They have always been adapted and changed. Fourth, we need more and better experimental data that can be used as a benchmark system. Fifth, cognitive theories can benefit from a computational modeling. Hence, both fields -- human and automated reasoning -- can both contribute to these milestones and are in fact a conditio sine qua non. Achievements in both fields can inform the others. Deviations between fields can inspire to seek a new and profound understanding of the nature of reasoning. Additionally to predict human inferences is a major step that can help to foster the integration of digital companions and cognitive assistance systems into our everyday life. An important condition is that such systems can adapt themselves to an individual's reasoning process and that such systems follow the principle of explainable AI to ensure trustfulness and to support the integration of results from other fields. Symbolic approaches do provide an easier access to it. This is the fifth workshop in a series of successful Bridging the Gap Between Human and Automated Reasoning workshops. Topics of interest include, but are not limited to the following: - limits and differences between automated and human reasoning - psychology of deduction and
[Hol-info] CADE-27: Second Call for Papers
Software (ThEdu'19), http://www.uc.pt/en/congressos/thedu/thedu19 The 6th Vampire Workshop CADE-27 ORGANIZERS Conference Chair: Elaine PimentelFederal University of Rio Grande do Norte, Brazil Organizers: Carlos Olarte Federal University of Rio Grande do Norte, Brazil Joao MarcosFederal University of Rio Grande do Norte, Brazil Claudia Nalon University of Brasilia, Brazil Giselle Reis CMU, Qatar Program Committee Chair: Pascal FontaineUniversite de Lorraine, CNRS, Inria, LORIA, France Workshop, Tutorial, and Competition Chair: Giles RegerUniversity of Manchester, UK Publicity Chair: Geoff SutcliffeUniversity of Miami, USA Program Committee: Carlos Areces, FaMAF - Universidad Nacional de Cordoba, Argentina Franz Baader, TU Dresden, Germany Clark Barrett, Stanford University, USA Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands Maria Paola Bonacina, Universita degli Studi di Verona, Italy Leonardo Mendonca de Moura, Microsoft Research, USA Hans de Nivelle, Nazarbayev University, Astana, Kazakhstan Clare Dixon, University of Liverpool, UK Mnacho Echenim, Universite de Grenoble, France Marcelo Finger, University of Sao Paulo, Brazil Pascal Fontaine, Universite de Lorraine, CNRS, Inria, LORIA, France Silvio Ghilardi, Universita degli Studi di Milano, Italy Juergen Giesl, RWTH Aachen University, Germany Rajeev Gore, The Australian National University, Australia Stefan Hetzl, Technische Universitaet Wien, Austria Marijn J. H. Heule, The University of Texas at Austin, USA Nao Hirokawa, JAIST, Japan Moa Johansson, Chalmers University of Technology, Sweden Cezary Kaliszyk, University of Innsbruck, Austria Deepak Kapur, University of New Mexico, USA Benjamin Kiesl, Technische Universitaet Wien, Austria Konstantin Korovin, The University of Manchester, UK Laura Kovacs, Technische Universitaet Wien, Austria Ramana Kumar, DeepMind, UK Claudia Nalon, University of Brasilia, Brazil Vivek Nigam, Federal University of Paraiba & Fortiss, Brazil & Germany Carlos Olarte, Federal University of Rio Grande do Norte, Brazil Jens Otten, University of Oslo, Norway Andre Platzer, Carnegie Mellon University, USA Andrew Reynolds, The University of Iowa, USA Philipp Ruemmer, Uppsala University, Sweden Renate A. Schmidt, The University of Manchester, UK Stephan Schulz, DHBW Stuttgart, Germany Roberto Sebastiani, University of Trento, Italy Natarajan Shankar, SRI International, USA Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau, Germany Martin Suda, Czech Technical University, Czech Republic Geoff Sutcliffe, University of Miami, USA Rene Thiemann, University of Innsbruck, Austria Uwe Waldmann, Max Planck Institute for Informatics, Germany Christoph Weidenbach, Max Planck Institute for Informatics, Germany Sarah Winkler, University of Innsbruck, Austria ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Artificial Intelligence and Theorem Proving, CFP
SECOND CALL FOR CONTRIBUTIONS Artificial Intelligence and Theorem Proving, AITP 2019 April 7-12, 2019, Obergurgl, Austria http://aitp-conference.org/2019 Deadline: December 1, 2018 https://easychair.org/conferences/?conf=aitp2019 BACKGROUND Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that. TOPICS - AI, machine learning and big-data methods in theorem proving and mathematics. - Collaboration between automated and interactive theorem proving. - Commonsense reasoning and reasoning in science. - Alignment and joint processing of formal, semi-formal, and informal libraries. - Methods for large-scale computer understanding of mathematics and science. - Combinations of linguistic/learning-based and semantic/reasoning methods - Formal verification of AI and machine learning algorithms, explainable AI. SESSIONS There will be several focused sessions on AI for ATP, ITP and mathematics, Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. CONFIRMED PARTICIPANTS/SPEAKERS Wolfgang Bibel, Darmstadt University of Technology Kevin Buzzard, Imperial College London Ben Goertzel, SingularityNET Georges Gonthier, INRIA Thomas C. Hales, University of Pittsburgh Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Michael Kinyon, University of Denver Angeliki Koutsoukou-Argyraki, University of Cambridge Ramana Kumar, DeepMind Sarah Loos, Google Research David McAllester, Toyota Technological Institute at Chicago Tomáš Mikolov, Facebook AI Research Scott Morrison, Australian National University Arnold Neumaier, University of Vienna Adam Pease, Infosys Joao Marques Silva, University of Lisbon Martin Suda, Czech Technical University in Prague Christian Szegedy, Google Research Robert Veroff, University of New Mexico CONTRIBUTED TALKS We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2019). DATES Submission deadline: December 1, 2018 Author notification: December 23, 2018 Conference registration: January 13, 2019 Camera-ready versions: February 1, 2019 Conference: April 7 - 12, 2019 POST-PROCEEDINGS We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR). PROGRAM COMMITTEE Jasmin Christian Blanchette, INRIA Nancy Ulrich Furbach, University of Koblenz Thomas C. Hales (co-chair), University of Pittsburgh Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Moa Johansson, Chalmers University Cezary Kaliszyk (co-chair), University of Innsbruck Michael Kohlhase, FAU Erlangen-Nürnberg Konstantin Korovin, The University of Manchester Ramana Kumar (co-chair), DeepMind Claudio Sacerdoti Coen, University of Bologna David McAllester, Toyota Technological Institute at Chicago Adam Pease, Infosys Stephan Schulz (co-chair), DHBW Stuttgart Geoff Sutcliffe, University of Miami Christian Szegedy, Google Research Josef Urban (co-chair), Czech Technical University in Prague LOCATION AND PRICE The conference will take place from April 7 to April 12 in the stunning scenery of the Tyrolean Alps in the Obergurgl Conference Center of the University of Innsbruck. Obergurgl is a picturesque village located at an altitude of 2000m, a 1-hour drive from Innsbruck. It offers a variety of winter-sport activities such as skiing, snowshoeing and hiking at this time of the year. The total price for accommodation in a twin room (based on 2-person occupancy), food and registration for the five days will be around 670 EUR. There are also several hotels in Obergurgl - booking early is recommended. ORGANIZERS Cezary Kaliszyk and Josef Urban ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] ICLA 2019: EIGHTH INDIAN CONFERENCE ON LOGIC AND ITS APPLICATIONS 2019
CALL FOR PAPERS ICLA 2019: EIGHTH INDIAN CONFERENCE ON LOGIC AND ITS APPLICATIONS 2019 Indian Institute of Technology Delhi New Delhi, India, March 3-5, 2019 Conference website http://icla2019.cse.iitd.ac.in Submission link https://easychair.org/conferences/?conf=icla2019 Poster download [1] The Association for Logic in India (ALI) announces the eighth edition of its biennial _International Conference on Logic and its Applications_ (ICLA), to be held at the Indian Institute of Technology Delhi from March 3 to 5, 2019. ICLA is a forum for bringing together researchers from a wide variety of fields in which formal logic plays a significant role, along with mathematicians, computer scientists, philosophers and logicians studying foundations of formal logic in itself. A special feature of this conference is the inclusion of studies in systems of logic in the Indian tradition and historical research on logic. As in the earlier events in this series, we shall have eminent scholars as invited speakers. Details of the last ICLA 2017 may be found at https://icla.cse.iitk.ac.in [2]. See http://ali.cmi.ac.in [3] for information on past events as well as updates on this conference. SCOPE: Authors are invited to submit papers presenting original and unpublished research in any area of logic and applications. Articles on mathematical and philosophical logic, logic in computer science, foundations and philosophy of mathematics and the sciences, use of formal logic in areas of theoretical computer science and artificial intelligence, logic and linguistics, history of logic, Indian systems of logic, or on the relationship between logic and other branches of knowledge, are welcome. COMMITTEES: PROGRAM COMMITTEE * Abhisekh Sankaran, IMSc Chennai * Amaldev Manuel, IIT Goa (CO-CHAIR) * Amit Kuber, IIT Kanpur * Anuj Dawar, University of Cambridge * Arnaud Sangnier, Univercite Paris Diderot * S. Arun-Kumar, IIT Delhi * Astrid Kiehn, IIT Mandi * Benedikt Löwe, University of Amsterdam * Benedikt Bollig, LSV, ENS Cachan, CNRS * Benjamin Monmege, Aix-Marseille Université, LIF, CNRS * Davide Grossi, University of Groningen * Denis Kuperberg, ENS Lyon * Gabriele Puppis, LaBRI, Bordeaux * Hans van Ditmarsch, LORIA - CNRS / University of Lorraine * Ivo Düntsch, Brock University * Katsuhiko Sano, Hokkaido University * M. Praveen, Chennai Mathematical Institute * Md. Aquil Khan, IIT Indore (CO-CHAIR) * Mihir Kumar Chakraborty, Jadavpur University * Minghui Ma, Sun Yat-Sen University * Ramchandra Phawade, IIT Dharwad * Richard Zach, University of Calgary * S. Akshay, IIT Bombay * Sankha Basu, IIIT Delhi * Smita Sirker, Jawaharlal Nehru University * Soma Dutta, University of Warmia and Mazury * Sreejith A. V., IIT Goa * Stefan Göller, University of Kassel * Sujata Ghosh, ISI Chennai * Sunil Easaw Simon, IIT Kanpur * Torben Braüner, Roskilde University ORGANIZING COMMITTEE * S. Arun-Kumar, IIT Delhi * Sanjiva Prasad, IIT Delhi * Subodh V Sharma, IIT Delhi CONFIRMED INVITED SPEAKERS: * Ian Pratt-Hartmann, University of Manchester * Carolin Antos, University of Konstanz * Martin Lange, University of Kassel * Mike Prest, University of Manchester * Johann A. Makowsky, Technion - Israel Institute of Technology Names of other speakers will be added soon. PUBLICATION: Submitted papers will be peer-reviewed and accepted papers will be published in the conference proceedings. The ICLA 2019 conference proceedings will be published in the Springer Lecture Notes in Computer Science (LNCS) series. [4] SUBMISSION GUIDELINES: Authors may submit drafts of full papers or extended abstracts. The submission must not exceed 12 pages in Springer-Verlag Lecture Notes LaTeX style. If appropriate, proof details omitted in the paper may be added in an appendix meant for the reviewers. Link: https://easychair.org/conferences/?conf=icla2019 Concurrent submissions to other conferences/journals are not admissible. For an accepted paper to be included in the proceedings, one of the authors must commit to presenting the paper at the conference. IMPORTANT DATES: Deadline for Submissions: 5 November 2018 15 NOVEMBER 2018 Notification to authors: 21 December 2018 Pre-conference Workshops: 1-2 March 2019 Conference: 3-5 March 2019 CONTACT: Please contact the PC chairs (aqu...@iiti.ac.in, a...@iitgoa.ac.in) for any further queries. Links: -- [1] https://easychair.org/cfp/poster_download.cgi?cfp=icla2019 [2] https://icla.cse.iitk.ac.in [3] http://ali.cmi.ac.in [4] http://www.dagstuhl.de/en/publications/lipics
[Hol-info] CADE-27: Call for Papers, Workshops, Tutorials and System Competitions
Chair: Giles RegerUniversity of Manchester, UK Publicity Chair: Geoff SutcliffeUniversity of Miami, USA Program Committee: Carlos Areces, FaMAF - Universidad Nacional de Cordoba, Argentina Franz Baader, TU Dresden, Germany Clark Barrett, Stanford University, USA Jasmin Christian Blanchette, Vrije Universiteit Amsterdam, The Netherlands Maria Paola Bonacina, Universita degli Studi di Verona, Italy Leonardo Mendonca de Moura, Microsoft Research, USA Hans de Nivelle, Nazarbayev University, Astana, Kazakhstan Clare Dixon, University of Liverpool, UK Mnacho Echenim, Universite de Grenoble, France Marcelo Finger, University of Sao Paulo, Brazil Pascal Fontaine, Universite de Lorraine, CNRS, Inria, LORIA, France Silvio Ghilardi, Universita degli Studi di Milano, Italy Juergen Giesl, RWTH Aachen University, Germany Rajeev Gore, The Australian National University, Australia Stefan Hetzl, Technische Universitaet Wien, Austria Marijn J. H. Heule, The University of Texas at Austin, USA Nao Hirokawa, JAIST, Japan Moa Johansson, Chalmers University of Technology, Sweden Cezary Kaliszyk, University of Innsbruck, Austria Deepak Kapur, University of New Mexico, USA Benjamin Kiesl, Technische Universitaet Wien, Austria Konstantin Korovin, The University of Manchester, UK Laura Kovacs, Technische Universitaet Wien, Austria Ramana Kumar, DeepMind, UK Claudia Nalon, University of Brasilia, Brazil Vivek Nigam, Federal University of Paraiba & Fortiss, Brazil & Germany Carlos Olarte, Federal University of Rio Grande do Norte, Brazil Jens Otten, University of Oslo, Norway Andre Platzer, Carnegie Mellon University, USA Andrew Reynolds, The University of Iowa, USA Philipp Ruemmer, Uppsala University, Sweden Renate A. Schmidt, The University of Manchester, UK Stephan Schulz, DHBW Stuttgart, Germany Roberto Sebastiani, University of Trento, Italy Natarajan Shankar, SRI International, USA Viorica Sofronie-Stokkermans, Universitaet Koblenz-Landau, Germany Martin Suda, Czech Technical University, Czech Republic Geoff Sutcliffe, University of Miami, USA Rene Thiemann, University of Innsbruck, Austria Uwe Waldmann, Max Planck Institute for Informatics, Germany Christoph Weidenbach, Max Planck Institute for Informatics, Germany Sarah Winkler, University of Innsbruck, Austria CALL FOR WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS The 27th International Conference on Automated Deduction (CADE-27) Natal, Brazil 25-30 August 2019 http://www.cade-27.info CALL FOR WORKSHOPS Workshop proposals for CADE-27 are solicited. The workshops will take place on August 25-26 2019, before the main conference. Both well-established workshops and newer ones are encouraged. Similarly, proposals for workshops with a tight focus on a core automated reasoning specialization, as well as those with a broader, more applied focus, are very welcome. Please provide the following information in your application document: + Workshop title. + Names and affiliations of organizers. + Proposed workshop duration (from half a day to two days) and preferred day(s). + Brief description of the goals and the scope of the workshop. Why is the workshop relevant for CADE? + Is the workshop new or has it met previously? In the latter case information on previous meetings should be given (e.g., links to the program, number of submissions, number of participants). + What are the plans for publication? CALL FOR TUTORIALS Tutorial proposals for CADE-27 are solicited. Tutorials are expected to be either half-day or full-day events, with a theoretical or applied focus, on a topic of interest for CADE-27. Proposals should provide the following information: + Tutorial title. + Names and affiliations of organizers. + Proposed tutorial duration (from half a day to one days) and the preferred day. + Brief description of the tutorial's goals and topics to be covered. + Whether or not a version of the tutorial has been given previously. CADE will take care of printing and distributing notes for tutorials that would like this service. CALL FOR SYSTEM COMPETITIONS The CADE ATP System Competition (CASC), which evaluates automated theorem proving systems for classical logics, has become an integral part of the CADE conferences. Further system competition proposals are solicited. The goal is to foster the development of automated reasoning systems in all areas relevant for automated deduction in a broader sense. Proposals should include the following information: + Competition title. + Names and affiliations of organizers. + Duration and schedule of the competition. + Room/space requirements. + Description of the competition task and the evaluation procedure. + Is the competition new or has it been organized before? In the latter case information on previous competitions should be given. + What computing resources are required and how will they be
[Hol-info] Artificial Intelligence and Theorem Proving, AITP 2019
CALL FOR CONTRIBUTIONS Artificial Intelligence and Theorem Proving, AITP 2019 April 7-12, 2019, Obergurgl, Austria http://aitp-conference.org/2019 Deadline: December 1, 2018 https://easychair.org/conferences/?conf=aitp2019 BACKGROUND Large-scale semantic processing and strong computer assistance of mathematics and science is our inevitable future. New combinations of AI and reasoning methods and tools deployed over large mathematical and scientific corpora will be instrumental to this task. The AITP conference is the forum for discussing how to get there as soon as possible, and the force driving the progress towards that. TOPICS - AI, machine learning and big-data methods in theorem proving and mathematics. - Collaboration between automated and interactive theorem proving. - Common-sense reasoning and reasoning in science. - Alignment and joint processing of formal, semi-formal, and informal libraries. - Methods for large-scale computer understanding of mathematics and science. - Combinations of linguistic/learning-based and semantic/reasoning methods - Formal verification of AI and machine learning algorithms, explainable AI SESSIONS There will be several focused sessions on AI for ATP, ITP and mathematics, Formal Abstracts, linguistic processing of mathematics/science, modern AI and big-data methods, and several sessions with contributed talks. The focused sessions will be based on invited talks and discussion oriented. CONFIRMED PARTICIPANTS/SPEAKERS (to be completed) Kevin Buzzard, Imperial College London Ben Goertzel, SingularityNET Georges Gonthier, INRIA Thomas C. Hales, University of Pittsburgh Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Michael Kinyon, University of Denver Angeliki Koutsoukou-Argyraki, University of Cambridge Ramana Kumar, DeepMind Sarah Loos, Google Research David McAllester, Toyota Technological Institute at Chicago Tomáš Mikolov, Facebook AI Research Arnold Neumaier, University of Vienna Martin Suda, Czech Technical University in Prague Christian Szegedy, Google Research Robert Veroff, University of New Mexico CONTRIBUTED TALKS We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pages formatted with easychair.cls. Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2019). DATES Submission deadline: December 1, 2018 Author notification: December 23, 2018 Conference registration: January 20, 2019 Camera-ready versions: February 1, 2019 Conference: April 7 - 12, 2019 POST-PROCEEDINGS We will consider an open call for post-proceedings in an established series of conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR). PROGRAM COMMITTEE (to be completed) Jasmin Christian Blanchette, INRIA Nancy Ulrich Furbach, University of Koblenz Thomas C. Hales (co-chair), University of Pittsburgh Sean Holden, University of Cambridge Mikoláš Janota, University of Lisbon Moa Johansson, Chalmers University Cezary Kaliszyk (co-chair), University of Innsbruck Michael Kohlhase, FAU Erlangen-Nürnberg Konstantin Korovin, The University of Manchester Ramana Kumar (co-chair), DeepMind Claudio Sacerdoti Coen, University of Bologna David McAllester, Toyota Technological Institute at Chicago Stephan Schulz (co-chair), DHBW Stuttgart Geoff Sutcliffe, University of Miami Christian Szegedy, Google Research Josef Urban (co-chair), Czech Technical University in Prague LOCATION AND PRICE The conference will take place from April 7 to April 12 in the stunning scenery of the Tyrolean Alps in the Obergurgl Conference Center of the University of Innsbruck. Obergurgl is a picturesque village located at an altitude of 2000m, a 1-hour drive from Innsbruck. It offers a variety of winter-sport activities such as skiing, snowshoeing and hiking at this time of the year. The total price for accommodation in a twin room (based on 2-person occupancy), food and registration for the five days will be around 600 EUR. There are also several hotels in Obergurgl - booking early is recommended. ORGANIZERS Cezary Kaliszyk and Josef Urban ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] A Second Opportunity to Submit - 13th International Workshop on the Implementation of Logics
The 13th International Workshop on the Implementation of Logics http://www.eprover.org/EVENTS/IWIL-2018.html CALL FOR PAPERS Second Phase Submission Deadline: October 11, 2018. Authors will be notified by: October 19th, 2018. The 13th International Workshop on the Implementation of Logics will be held on 16th November 2018, in conjunction with the 22nd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, at the Haile Resort in Awassa, Ethiopia. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: + Propositional logic and decision procedures, including SMT + First-order and higher order logics + Non-classical logics, including modal, temporal, description, non-monotonic reasoning + Formal foundations for efficient implementation of logics + Data structures and algorithms for the efficient representation and processing of logical concepts + Proof/model search organization and heuristics for logical reasoning systems + Data analysis and machine learning approaches to search control + Techniques for proof/model search visualization and analysis + Reasoning with ontologies and other large theories + Implementation of efficient theorem provers and model finders for different logics + System descriptions of logical reasoning systems + Issues of reliability, witness generation, and witness verification + Evaluation and benchmarking of provers and other logic-based systems + I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15 pages) via the EasyChair page for IWIL-2018. https://easychair.org/conferences/?conf=iwil2018 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. The proceedings will be published as a volume of Kalpa Publications in Computing. Important Dates: First phase: + Submission of papers/abstracts: October 1st, 2018 + Notification of acceptance: October 12th, 2018 Second phase: + Submission of papers/abstracts: October 11st, 2018 + Notification of acceptance: October 19th, 2018 + Camera ready versions due: October 29th, 2018 + Workshop:November 16th, 2018 Program committee: Konstantin Korovin (Co-Chair) University of Manchester Stephan Schulz (Co-Chair) DHBW Stuttgart Martin Suda (Co-Chair) Czech Technical University in Prague Armin BiereJohannes-Kepler Universitaet Linz Jasmin Christian BlanchetteVrije Universiteit Amsterdam, LORIA Nancy Pascal FontaineUniversite de Lorraine, CNRS, Inria, LORIA Yevgeny KazakovUlm University Jens Otten University of Oslo Giles RegerUniversity of Manchester Andrew ReynoldsUniversity of Iowa Martina Seidl Johannes-Kepler Universit??t Linz Alexander SteenFreie Universitaet Berlin Geoff SutcliffeUniversity of Miami Josef UrbanCzech Technical University ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-22 in Ethiopia - Call for Short Papers
** The 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-22 Haile Resort, Awassa, Ethiopia http://www.LPAR-22.info CALL FOR SHORT PRESENTATION PAPERS In keeping with the tradition of LPAR, researchers and practitioners are invited to submit short presentation papers (the papers can be full length, the presentation slots will be short), reporting on interesting work in progress, system and tool descriptions, experimental results, etc. They need not be original, and extended or revised versions of the papers may be submitted concurrently with or after LPAR to another conference or a journal. Authors of accepted papers are required to ensure that at least one of them will be present at the conference. Papers that do not adhere to this policy will not be published. The short presentation papers will be published electronically as a volume in the Kalpa series, see http://www.easychair.org/publications/Kalpa. The LaTeX and Microsoft Word templates for the Kalpa series can be downloaded from http://www.easychair.org/publications/for_authors. Papers may be up to 15 pages long, and must be submitted through the EasyChair system using the web page https://easychair.org/conferences/?conf=lpar22 Paper submission deadline: 3rd October 2018 Notification of acceptance: 10th October 2018 Final version: 17th October 2018 ... however, in order to facilitate authors making travel arrangements, papers submitted before the deadline will be reviewed immediately, and a decision made in approximately one week. Submit early, and submit often! ** ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 13th International Workshop on the Implementation of Logics
The 13th International Workshop on the Implementation of Logics http://www.eprover.org/EVENTS/IWIL-2018.html CALL FOR PAPERS Deadline: October 1, 2018. The 13th International Workshop on the Implementation of Logics will be held on 16th November 2018, in conjunction with the 22nd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, at the Haile Resort in Awassa, Ethiopia. We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: + Propositional logic and decision procedures, including SMT + First-order and higher order logics + Non-classical logics, including modal, temporal, description, non-monotonic reasoning + Formal foundations for efficient implementation of logics + Data structures and algorithms for the efficient representation and processing of logical concepts + Proof/model search organization and heuristics for logical reasoning systems + Data analysis and machine learning approaches to search control + Techniques for proof/model search visualization and analysis + Reasoning with ontologies and other large theories + Implementation of efficient theorem provers and model finders for different logics + System descriptions of logical reasoning systems + Issues of reliability, witness generation, and witness verification + Evaluation and benchmarking of provers and other logic-based systems + I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full paper (up to 15 pages) via the EasyChair page for IWIL-2018. https://easychair.org/conferences/?conf=iwil2018 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. The proceedings will be published as a volume of Kalpa Publications in Computing. Important Dates: + Submission of papers/abstracts: October 1st, 2018 + Notification of acceptance: October 12th, 2018 + Camera ready versions due: October 29th, 2018 + Workshop:November 16th, 2018 Program committee (so far - more coming): Konstantin Korovin (Co-Chair) University of Manchester Stephan Schulz (Co-Chair) DHBW Stuttgart Martin Suda (Co-Chair) Czech Technical University in Prague Geoff SutcliffeUniversity of Miami ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-22 Ethiopia - Call for Papers
The 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-22 Awassa, Ethiopia, 16-21 November 2018 http://www.LPAR-22.info CALL FOR PAPERS The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 22nd LPAR will be held will be held in Haile Resort, Awassa, Ethiopia, 16-21 November 2018. The proceedings will be published by EasyChair Publications, in the EPiC Series in Computing. The volume will be open access and the authors will retain copyright. ==Important Dates Abstract submission6th August 2018 Paper submission 13th August 2018 Notification 24th September 2018 Final version 15th October 2018 Early registration 15th October 2018 Workshops 16th November 2018 Conference 17-21st November 2018 ==Topics New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: + Abduction and interpolation methods + Answer set programming + Automated reasoning + Constraint programming + Contextual reasoning + Decision procedures + Description logics + Foundations of security + Hardware verification + Implementations of logic + Inconsistency- and exception tolerant reasoning + Interactive theorem proving + Knowledge representation and reasoning + Logic and computational complexity + Logic and databases + Logic and games + Logic and machine learning + Logic and the web + Logic and types + Logic in artificial intelligence + Logic of distributed systems + Logic of knowledge and belief + Logic programming + Logical aspects of concurrency + Logical foundations of programming + Modal and temporal logics + Model checking + Non-monotonic reasoning + Ontologies and large knowledge bases + Paraconsistent logics + Probabilistic and fuzzy reasoning + Program analysis + Rewriting + Satisfiability checking + Satisfiability modulo theories + Software verification + Specification using logic + Unification theory ==Organization Program Chairs: Gilles Barthe (IMDEA Software Institute) Margus Veanes (Microsoft Research) Martin Hofmann (Ludwig-Maximilians-Universität München, in memoriam) Conference Chair: Geoff Sutcliffe (University of Miami, USA) ==Submission Details Submissions of two kinds are welcome: - Regular papers that describe solid new research results. They can be up to 15 pages long in EasyChair style, including figures but excluding references and appendices (that reviewers are not required to read). - Experimental and tool papers that describe implementations of systems, report experiments with implemented systems, or compare implemented systems. They can be up to 8 pages long in the EasyChair style. Both types of papers must be electronically submitted in PDF via EasyChair: https://easychair.org/conferences/?conf=lpar22 Authors must register a title and an abstract by the abstract submission deadline. ==Participation Authors of accepted papers are required to ensure that at least one of them will be present at the conference. ==Workshop Proposals Proposals for workshops to be held in conjunctionwith LPAR-22 are solicited. Please email proposals to the program and conference chairs. For more details about the venue and organization, see the conference webpage http://www.LPAR-22.info -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] LPAR-22 in Ethiopia - Call for Papers and Workshops
The 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning LPAR-22 Awassa, Ethiopia, 16-21 November 2018 http://www.LPAR-22.info CALL FOR PAPERS The series of International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) is a forum where, year after year, some of the most renowned researchers in the areas of logic, automated reasoning, computational logic, programming languages and their applications come to present cutting-edge results, to discuss advances in these fields, and to exchange ideas in a scientifically emerging part of the world. The 22nd LPAR will be held will be held in Haile Resort, Awassa, Ethiopia, 16-21 November 2018. The proceedings will be published by EasyChair Publications, in the EPiC Series in Computing. The volume will be open access and the authors will retain copyright. ==Important Dates Abstract submission6th August 2018 Paper submission 13th August 2018 Notification 24th September 2018 Final version 15th October 2018 Early registration 15th October 2018 Workshops 16th November 2018 Conference 17-21st November 2018 ==Topics New results in the fields of computational logic and applications are welcome. Also welcome are more exploratory presentations, which may examine open questions and raise fundamental concerns about existing theories and practices. Topics of interest include, but are not limited to: + Abduction and interpolation methods + Answer set programming + Automated reasoning + Constraint programming + Contextual reasoning + Decision procedures + Description logics + Foundations of security + Hardware verification + Implementations of logic + Inconsistency- and exception tolerant reasoning + Interactive theorem proving + Knowledge representation and reasoning + Logic and computational complexity + Logic and databases + Logic and games + Logic and machine learning + Logic and the web + Logic and types + Logic in artificial intelligence + Logic of distributed systems + Logic of knowledge and belief + Logic programming + Logical aspects of concurrency + Logical foundations of programming + Modal and temporal logics + Model checking + Non-monotonic reasoning + Ontologies and large knowledge bases + Paraconsistent logics + Probabilistic and fuzzy reasoning + Program analysis + Rewriting + Satisfiability checking + Satisfiability modulo theories + Software verification + Specification using logic + Unification theory ==Organization Program Chairs: Gilles Barthe (IMDEA Software Institute) Margus Veanes (Microsoft Research) Martin Hofmann (Ludwig-Maximilians-Universität München, in memoriam) Conference Chair: Geoff Sutcliffe (University of Miami, USA) ==Submission Details Submissions of two kinds are welcome: - Regular papers that describe solid new research results. They can be up to 15 pages long in EasyChair style, including figures but excluding references and appendices (that reviewers are not required to read). - Experimental and tool papers that describe implementations of systems, report experiments with implemented systems, or compare implemented systems. They can be up to 8 pages long in the EasyChair style. Both types of papers must be electronically submitted in PDF via EasyChair: https://easychair.org/conferences/?conf=lpar22 Authors must register a title and an abstract by the abstract submission deadline. ==Participation Authors of accepted papers are required to ensure that at least one of them will be present at the conference. ==Workshop Proposals Proposals for workshops to be held in conjunctionwith LPAR-22 are solicited. Please email proposals to the program and conference chairs. For more details about the venue and organization, see the conference webpage http://www.LPAR-22.info -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 23rd International Conference on Engineering Complex Systems - Call for Papers
CALL FOR PAPERS The 23rd International Conference on Engineering Complex Systems ICECCS 2018 12-14 December 2018 - Melbourne, Australia http://formal-analysis.com/iceccs/2018/ Important Dates (AoE time) Abstract submission:15th June 2018 Paper submission: 22nd June 2018 Notification of acceptance: 22th August 2018 Camera ready copy due: 21th September 2018 We have seen a rapid rising emphasis on design, implement and manage complex computer systems which are present in every aspect of human activities, such as manufacturing, communications, defense, transportation, aerospace, hazardous environments, energy, and health care. The complex computer systems are frequently distributed over heterogeneous networks and processing large amount data. Complexity arises from many factors, including the dynamic environments and scenarios these systems operate in; demanding and sometimes conflicting requirements in functionality, efficiency, scalability, security, dependability, inoperability and adaptability; as well as the large variation in development methodology, programming languages and implementation details. The key issues in these systems include performance, real-time behavior, fault tolerance, security, adaptability, development time and cost, and long life concerns. The goal of this conference is to bring together industrial, academic, and government experts, from a variety of application domains and software disciplines, to discuss how the disciplines' problems and solution techniques interact within the whole system. Researchers, practitioners, tool developers and users, and technology transfer experts are all welcome. The scope of interest includes long-term research issues; near-term requirements and challenges; established complex systems; emerging promising tools; and retrospective and prospective reflections of research and development into complex systems. Scope and Topics Authors are invited to submit papers describing original, unpublished research results, case studies and tools. Papers are solicited in all areas related to complex computer-based systems, including the causes of complexity and means of avoiding, controlling, or coping with complexity. Topic areas include, but are not limited to: Requirement specification and analysis Verification and validation Security and privacy of complex systems Model-driven development Reverse engineering and refactoring Software architecture Big Data Management Ambient intelligence, pervasive computing Ubiquitous computing, context awareness, sensor networks Design by contract Agile methods Safety-critical & fault-tolerant architectures Adaptive, self-managing and multi-agent systems Real-time, hybrid and embedded systems Systems of systems Cyber-physical systems and Internet of Things (IoT) Tools and tool integration Industrial case studies Applications to SAT/SMT techniques to analysis of complex systems Different kinds of contributions are sought, including novel research, lessons learned, experience reports, and discussions of practical problems faced by industry and user domains. The ultimate goal is to build a rich and comprehensive conference program that can fit the interests and needs of different classes of attendees: professionals, researchers, managers, and students. A program goal is to organize several sessions that include both academic and industrial papers on a given topic and culminate panels to discuss relationships between industrial and academic research. Full Papers Full papers are divided into two categories: Technical Papers and Experience Reports. The papers submitted to both categories will be reviewed by program committee members, and papers accepted in either category will be published in the conference proceedings. Technical papers should describe original research, and experience reports should present practical projects carried out in industry, and reflect on the lessons learnt from them. Short Papers Short paper submissions describe early-stage, ongoing or PhD research. All short papers will be reviewed by program committee members, and accepted short papers will be published in the conference proceedings. Paper Submissions Submitted manuscripts should be in English and formatted in the style of the double-column CPS format. Full papers should not exceed 10 pages, and short papers should not exceed 4 pages, including figures, references, and appendices. All submissions should be in PDF format. Submissions not adhering to the specified format and length may be rejected immediately, without review. Please prepare your manuscripts in accordance to the CPS guidelines: http://www.ieee.org/conferences_events/conferences/publishing/templates.html. We invite all prospective authors to submit their
[Hol-info] CASC-J9 - the ATP System Competition
--- CASC-J9 - The CADE ATP System Competition to be held at The 9th International Joint Conference on Automated Reasoning Oxford, United Kingdom, 14th-17th July 2018 The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J9 will be held on the 14th July 2018, during the 9th International Joint Conference on Automated Reasoning. CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of: + the number of problems solved, and + the number of problems solved with a solution output, and + the average runtime for problems solved; in the context of: + a bounded number of eligible problems, chosen from the TPTP library, and + specified time limits for solution attempts. The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. Further details and registration information are available at: http://www.tptp.org/CASC/J9/ Registration of systems for CASC-J9 is now invited. System registration closes on 11th June. Please register early so that adequate resources can be allocated. DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! --- -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CASC-J9 - the ATP System Competition - Call for Systems
--- CASC-J9 - The CADE ATP System Competition to be held at The 9th International Joint Conference on Automated Reasoning Oxford, United Kingdom, 14th-17th July 2018 The CADE and IJCAR conferences are the major forums for the presentation of new research in all aspects of automated deduction. In order to stimulate ATP research and system development, and to expose ATP systems within and beyond the ATP community, the CADE ATP System Competition (CASC) is held at each CADE and IJCAR conference. CASC-J9 will be held on the 14th July 2018, during the 9th International Joint Conference on Automated Reasoning. CASC evaluates the performance of sound, fully automatic, ATP systems. The evaluation is in terms of: + the number of problems solved, and + the number of problems solved with a solution output, and + the average runtime for problems solved; in the context of: + a bounded number of eligible problems, chosen from the TPTP library, and + specified time limits for solution attempts. The competition organizer is Geoff Sutcliffe. The competition is overseen by a panel of knowledgeable researchers who are not participating in the event. Further details and registration information are available at: http://www.tptp.org/CASC/J9/ Registration of systems for CASC-J9 is now invited. System registration closes on 11th June. Please register early so that adequate resources can be allocated. DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! DO IT NOW! --- -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IJCAR 2018: Woody Bledsoe Student Travel Awards - Call for Applications
Woody Bledsoe Student Travel Awards at IJCAR 2018 Call for Applications The Woody Bledsoe Student Travel Award was created to honour the memory of Woody Bledsoe, for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to enable selected students to attend the International Conference on Automated Deduction (CADE) or the International Joint Conference on Automated Reasoning (IJCAR), whichever is scheduled for the year, by covering part of their expenses. The winners of the IJCAR 2018 Woody Bledsoe Student Travel Award will be partially reimbursed (up to value of 900 EUR, depending on needs and available funds) for their conference registration, transportation, and accommodation expenses. A nomination consists of a recommendation letter of up to 300 words from the student's adviser. Nominations for IJCAR 2018 should be sent by e-mail to the Program Committee Chairs (Didier Galmiche, Stephan Schulz and Roberto Sebastiani) at ijcar2...@easychair.org. Please include "Woody Bledsoe 2018 Application" in your subject line. The nomination letter should contain: - name of the student, - whether the student is an author of a paper accepted to IJCAR or submitted to an IJCAR workshop, or contributor to a system in the CASC competition - an explanation of the potential benefit of the IJCAR attendance to the student - a statement regarding the dependence of the student on the award for attendance, including any special circumstances Nominations must arrive no later than May 18, 2018. The winners will be notified by June 1st, 2018. Note that FLoC/IJCAR early registration ends on June 6th. The awards will be presented at IJCAR 2018; in case a winner does not attend, the chairs may transfer the award to another nominee or give no award. The awards are sponsored by CADE Inc. -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] CICM 2018 - Call for Papers
Call for Papers formal papers - informal papers - doctoral programme 11th Conference on Intelligent Computer Mathematics - CICM 2018 - August 13-17, 2018 RISC, Hagenberg, Austria http://www.cicm-conference.org/2018 Digital and computational solutions are becoming the prevalent means for the generation, communication, processing, storage and curation of mathematical information. CICM brings together the many separate communities that have developed theoretical and practical solutions for mathematical applications such as computation, deduction, knowledge management, and user interfaces. It offers a venue for discussing problems and solutions in each of these areas and their integration. CICM 2018 will feature 3 invited speakers * Akiko Aizawa, National Institute of Informatics, University of Tokyo * Bruno Buchberger, Research Institute for Symbolic Computation, Johannes Kepler University * Adri Olde Daalhuis, University of Edinburgh and 5 affiliated workshops * Computer Algebra in the age of Types * Computer Mathematics in Education - Enlightenment or Incantation * Formal Mathematics for Mathematicians * Formal Verification of Physical Systems * Mathematical Models and Mathematical Software as Research Data We invite submissions in all topics relating to intelligent computer mathematics, in particular but not limited to * theorem proving and computer algebra * mathematical knowledge management * digital mathematical libraries CICM appreciates the varying nature of the relevant research in this area and invites submissions of very different forms: 1) Formal submissions will be reviewed rigorously and accepted papers will be published in a volume of Springer LNAI: * regular papers (up to 15 pages) present novel research results * project and survey papers (up to 15 pages + bibliography) summarize existing results * system and dataset descriptions (up to 5 pages) present digital artifacts 2) Informal submissions will be reviewed with a positive bias and selected for presentation based on their relevance for the community. * informal papers may present work-in-progress, project announcements, position statements, etc. * posters, mini-tutorials, and system demos will be presented in special sessions 3) The doctoral programme provides PhD students a forum to present early results receive constructive feedback and mentoring. * Important Dates * Formal submissions - Abstract deadline:April 15 - Full paper deadline: April 22 - Reviews sent to authors: May 21 - Rebuttals due:May 27 - Notification of acceptance: June 4 - Camera-ready copies due: June 8 - Conference: August 13-17 Informal submissions and doctoral programme Two separate submission rounds are offered so that some authors can make early travel plans while others submit spontaneously. - First round submission deadline: April 22 - Second round submission deadline: July 31 All submissions should be made via easychair at https://easychair.org/conferences/?conf=cicm2018 -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] Bridging the Gap between Human and Automated Reasoning
Fourth Workshop on Bridging the Gap between Human and Automated Reasoning a FAIM workshop (supported by IFIP TC12) Stockholm, Sweden Reasoning is a core ability in human cognition. Its power lies in the ability to theorize about the environment, to make implicit knowledge explicit, to generalize given knowledge and to gain new insights. There are a lot of findings in cognitive science research which are based on experimental data about reasoning tasks, among others models for the Wason selection task or the suppression task discussed by Byrne and others. This research is supported also by brain researchers, who aim at localizing reasoning processes within the brain. Early work often used propositional logic as a normative framework. Any deviation from it has been considered an error. Central results like findings from the Wason selection task or the suppression task inspired a shift from propositional logic and the assumption of monotonicity in human reasoning towards other reasoning approaches. This includes but is not limited to models using probabilistic approaches, mental models, or non-monotonic logics. Considering cognitive theories for syllogistic reasoning show that none of the existing theories is close to the existing data. But some formally inspired cognitive complexity measures can predict human reasoning difficulty for instance in spatial relational reasoning. Automated deduction, on the other hand, is mainly focusing on the automated proof search in logical calculi. And indeed there is tremendous success during the last decades. Recently a coupling of the areas of cognitive science and automated reasoning is addressed in several approaches. For example there is increasing interest in modeling human reasoning within automated reasoning systems including modeling with answer set programming, deontic logic or abductive logic programming. There are also various approaches within AI research for common sense reasoning and in the meantime there even exist benchmarks for commonsense reasoning, like the Winograd and the COPA challenge. Despite a common research interest - reasoning - there are still several milestones necessary to foster a better interdisciplinary research. First, to develop a better understanding of methods, techniques, and approaches applied in both research fields. Second, to have a synopsis of the relevant state-of-the-art in both research directions. Third, to combine methods and techniques from both fields and find synergies. E.g., techniques and methods from computational logic have never been directly applied to model adequately human reasoning. They have always been adapted and changed. Fourth, we need more and better experimental data that can be used as a benchmark system. Fifth, cognitive theories can benefit from a computational modeling. Hence, both fields - human and automated reasoning - can both contribute to these milestones and are in fact a conditio sine qua non. Achievements in both fields can inform the others. Deviations between fields can inspire to seek a new and profound understanding of the nature of reasoning. This is the fourth workshop in a series of successful Bridging the Gap Between Human and Automated Reasoning workshops. Topics of interest include, but are not limited to the following: - benchmark problems relevant in both fields - approaches to tackle Benchmark problems like the Winograd Schema Challenge or the COPA challenge - limits and differences between automated and human reasoning - psychology of deduction and common sense reasoning - logics modeling human reasoning - non-monotonic, defeasible, and classical reasoning The workshop is part of the FAIM workshop program located at the Federated Artificial Intelligence Meeting (FAIM) which includes the major conferences IJCAI, ECAI, ICML, AAMAS, ICCBR and SoCS. The Bridging workshop is supported by IFIP TC12. IMPORTANT DATES Full Paper submission deadline: 25th of April, 2018 Notification: 3rd of June, 2018 Final submission: 17th of June, 2018 Workshop: July 2018 SUBMISSION AND CONTRIBUTION FORMAT Papers, including the description of work in progress are welcome and should be formatted according to IJCAI guidelines. The length should not exceed 6 pages excluding references. All papers must be submitted in PDF. Formatting instructions and the style files can be obtained from http://www.ijcai.org/authors_kit. The EasyChair submission site is available at: https://easychair.org/conferences/?conf=bridging2018 PROCEEDINGS Proceedings of the workshop will be published as CEUR workshop proceedings. ORGANIZERS Ulrich Furbach, University of Koblenz Sageet Khemlani, Naval Research Laboratory, Washington DC Oliver Obst, Western Sydney University Marco Ragni, University of Freiburg Claudia Schon, University of Koblenz PROGRAM COMMITTEE - Emmanuelle Diez Saldanha, University of Dresden - Ulrich Furbach, University of Koblenz - Steffen Hoelldobler, University of Dresden - Antonis C. Kakas,
[Hol-info] Verification and Deduction Mentoring Workshop 2018
Verification and Deduction Mentoring Workshop 2018, FLoC 2018, July 13, 2018 CALL FOR PARTICIPATION ***Overview*** The purpose of the Verification and Deduction Mentoring Workshop is to provide mentoring and career advice to early-stage graduate students, to attract them to pursue research careers in the area of computer-aided verification and deduction. The workshop will particularly encourage participation of women and underrepresented minorities. This mentoring workshop unites the 4th Verification Mentoring Workshop and the 1st Deduction Mentoring Workshop, and is affiliated both with CAV 2018 and IJCAR 2018. The workshop program will include a number of invited talks and interactive sessions. The invited talks will give an overview of the field, highlight career challenges and give advices on career planning. The invited talks will focus both on academia and industry. ***Application and Participation*** Graduate and undergraduate (seniors only) students interested in attending our workshop are requested to apply at: http://cavconference.org/2018/verification-deduction-mentoring-workshop/ We have limited funding available to support students attending the mentoring workshop and CAV/IJCAR 2018. ***Deadline for submission of applications*** April 13, 2018 -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] PAAR 2018 - Call for Papers
** PAAR-2018: 6TH WORKSHOP ON PRACTICAL ASPECTS OF AUTOMATED REASONING Oxford, UK, July 19, 2018 Submission link: https://easychair.org/conferences/?conf=paar2018 Abstract registration deadline: April 8, 2018 Submission deadline: April 15, 2018 Topics: automated reasoning, implementation, tools ** PAAR provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. The workshop will bring together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. It will allow researchers to present their work in progress, and to discuss new implementation techniques and applications. Submission Guidelines - Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages) via EasyChair at https://easychair.org/conferences/?conf=paar2018. Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. Submissions should be prepared in LaTeX using the EasyChair proceedings style. The package containing the class file and its user guide and some helper tools can be downloaded from http://www.easychair.org/publications/easychair.zip. Topics include, but are not limited to: -- * automated reasoning in propositional, first-order, higher-order, and non-classical logics; * implementation of provers (SAT, SMT, resolution, tableau, instantiation- based, rewriting, logical frameworks, etc.); * automated reasoning tools for all kinds of practical problems and applications; * pragmatics of automated reasoning within proof assistants; * practical experiences, usability aspects, feasibility studies; * evaluation of implementation techniques and automated reasoning tools; * performance aspects, benchmarking approaches; non-standard approaches to automated reasoning, non*standard forms of automated reasoning, new applications; * implementation techniques, optimisation techniques, strategies and heuristics, fairness; * tools or methods that support prover development; * system descriptions and demos. Programme Committee --- * Haniel Barbosa, The University of Iowa , USA * Simon Cruanes, Aesthetic Integration, USA * Pascal Fontaine, Loria, INRIA, University of Lorraine, France * Martin Giese, University of Oslo, Norway * Alberto Griggio, Fondazione Bruno Kessler, Italy * Marijn Heule, The University of Texas at Austin, USA * Dejan Jovanovic, SRI International, USA * Chantal Keller, LRI, Université Paris-Sud, France * Boris Konev (co-chair), University of Liverpool, UK * Konstantin Korovin, The University of Manchester, UK * Laura Kovacs, Vienna University of Technology, Austria * Cláudia Nalon, University of BrasÃlia, Brasil * Jens Otten, University of Oslo, Norway * Giles Reger, The University of Manchester, UK * Andrew Reynolds, University of Iowa, USA * Philipp Ruemmer (co-chair), Uppsala University, Sweden * Martin Suda, Vienna University of Technology, Austria * Mattias Ulbrich, Karlsruhe Institute of Technology, Germany * Josef Urban (co-chair), Czech Technical University, CZ Publication --- PAAR proceedings will be published electronically in the EasyChair Proceedings in Computing (EPiC) series or in the CEUR workshop proceedings. Venue - Oxford, UK Important dates --- Abstract registration deadline: April 8, 2018 Submission deadline: April 15, 2018 Workshop: July 19, 2018 -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] RuleML+RR 2018 SECOND CALL FOR PAPERS
== RuleML+RR 2018 SECOND CALL FOR PAPERS RuleML+RR 2018: International Joint Conference on Rules and Reasoning http://2018.ruleml-rr.org Part of Luxembourg Logic for AI Summit (LuxLogAI, https://luxlogai.uni.lu) == == SUMMARY == High-quality papers related to theoretical advances, novel technologies, and innovative applications concerning knowledge representation and reasoning with rules are solicited. Important dates: - Abstract: 20 Apr 2018 - Full paper: 27 Apr 2018 == THE CONFERENCE == The International Joint Conference on Rules and Reasoning (RuleML+RR) is the leading international joint conference in the field of rule-based reasoning. Stemming from the synergy between the well-known RuleML and RR events, one of the main goals of this conference is to build bridges between academia and industry. RuleML+RR 2018 aims to bring together rigorous researchers and inventive practitioners, interested in the foundations and applications of rules and reasoning in academia, industry, engineering, business, finance, healthcare and other application areas. It will provide a forum for stimulating cooperation and cross-fertilization between the many different communities focused on the research, development and applications of rule-based systems. RuleML+RR 2018 will take place in Luxembourg on September 18th-21th 2018 and will be part of the Luxembourg Logic for AI Summit (LuxLogAI) "Methods and Tools for Responsible AI", bringing together RuleML+RR 2018, DecisionCAMP 2018, the Reasoning Web Summer School (RW 2018), and the Global Conference on Artificial Intelligence (GCAI 2018). == TOPICS == RuleML+RR welcomes original research from all areas of Rules and Reasoning. Topics of particular interest include: * Rule-based languages for intelligent information access and for the semantic web * Vocabularies, ontologies, and business rules * Ontology-based data access * Data management, and data interoperability for web data * Distributed agent-based systems for the web * Scalability and expressive power of logics for the semantic web * Reasoning with incomplete, inconsistent and uncertain data * Non-monotonic, common-sense, and closed-world reasoning for web data * Non-classical logics and the Web * Constraint programming * Logic programming * Production & business rules systems * Streaming data and complex event processing * Rules for machine learning, knowledge extraction and information retrieval * Rule-based approaches to natural language processing * Rule discovery, extraction and transformation * Rules and ontology learning * Deep Learning for rules and ontologies * Neural Networks and logic rules * Neural Networks and ontologies * Rule-based approaches to agents * Higher-order and modal rules * Rules for knowledge graphs * Pragmatic web reasoning and distributed rule inference / rule execution * Big data reasoning with rules * Rule markup languages and rule interchange formats * Rule-based policies, reputation, and trust * Scalability and expressive power of logics for rules * System descriptions, applications and experiences * Rules and human language technology * Rules in online market research and online marketing * Applications of rule technologies in healthcare and life sciences * Applications of rule technologies in law, regulation and finance * Industrial applications of rules * Rules and social media * Rules of ethics, laws, policies, and regulations Particularly encouraged are submissions that combine one or several of the above topics with the overall focus theme of the LuxLogAI Summit: Methods and Tools for Responsible AI == SUBMISSIONS == We accept the following submission formats for papers: * Full papers (up to 15 pages in LNCS style) * Technical Communications (up to 8 pages in LNCS style) Submitted full papers should present original and significant research results. They must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference/workshop with formal proceedings. Double submission to a workshop with informal proceedings is allowed. Technical communications are intended for promising but possibly preliminary work, position papers, system descriptions, and applications descriptions (which may be accompanied by a demo). Submissions: via EasyChair ( https://easychair.org/conferences/?conf=rulemlrr2018) The RuleML+RR 2018 best papers will be invited for rapid publication in the Journal of Theory and Practice of Logic Programming (TPLP). In addition to regular submissions, RuleML+RR 2018 will host an Industry Track, a Doctoral Consortium and the 12th International Rule Challenge. == PUBLICATION == The conference proceedings will be published by Springer in the Lecture Notes in Computer Science series (LNCS). All submissions must be prepared in Springer's LaTeX style LNCS (
[Hol-info] SAT/SMT/AR Summer School 2018
SAT/SMT/AR Summer School 2018 We are pleased to announce that the next edition of the SAT/SMT/AR Summer School will take place in Manchester, UK on 3-6th July 2018. Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR) continue to make rapid advances and find novel uses in a wide variety of applications, both in computer science and beyond. The SAT/SMT/AR Summer School aims to bring a select group of students up to speed quickly in this exciting research area. The school continues the successful line of Summer Schools that ran from 2011 to 2015 as SAT/SMT Summer Schools and added AR in 2016. There will also be a special session on computer algebra to continue the activity of the SC2 summer school in 2017. Lecturers for this year's summer school have been announced on the school's website http://ssa-school-2018.cs.manchester.ac.uk/index.php/speakers/ and detailed programme of topics will appear soon. Applications can be made via the following form https://goo.gl/forms/e2hgn5GbnPROMTEK2 -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] IfCoLog JLA - Reasoning on Legal Texts
IfCoLog Journal of Logics and their Applications Special issue "Reasoning on Legal Texts" ** Paper submission deadline: Jul 31st, 2018 ** Guest editors: Livio Robaldo - University of Luxembourg (Luxembourg) Sotiris Batsakis - University of Huddersfield (UK) Maria Vanina Martinez - Universidad Nacional del Sur (Argentina) Christoph Benzmueller - Freie Universitaet Berlin (Germany) Regulations are a widespread and important part of governments and businesses. They encode how products are manufactured, and how the processes are to be performed. Such regulations, in general, are difficult to understand and apply. Undoubtedly, the law, for example, as the reflection of human society, presents the broadest range of expression and interpretation, since the interpretation of even the most common words becomes problematic. Even individual regulations may be self-contradictory as a result of their gradual development process, as well as the lack of a formal drafting process. In an increasingly complicated environment, as well as regulatory review, automated reasoning processes become more and more necessary. Current state-of-the-art technologies enforce reasoning applications on legal texts such as decision making and compliance checking starting from logical and/or ontology-based representations of norms. These semantic representations are typically obtained via Natural Language Processing (NLP) in an automatic fashion, in order to avoid huge time-consuming manual effort. To bridge such challenges, several research projects in the legal domain have been recently funded by the EU and similar institutions, among which is "MIREL: MIning and REasoning with Legal texts". The aim of the MIREL project is to bridge the gap between the community working on legal ontologies and NLP methods applied to legal documents, and the community working on reasoning methods and formal logic, towards the objectives described above. This special issue focuses on legal reasoning, thus welcoming submissions describing novel approaches for reasoning in the legal domain starting from logical or ontology-based representations of legal knowledge. A non-exhaustive list of topics includes: - Logical formalization of legal knowledge - Norm enforcement and compliance - Decision making methods and applications - Computational methods for legal reasoning - Legal argumentation - Dynamics of normative knowledge - Formal models of norms, normative systems, and norm-governed societies - Using logic formalisms and technologies in large legal document collections - Legislative and case-law metadata models - Semantic annotations for legal texts - Inconsistency handling and exception-tolerant reasoning - Legal reasoning under uncertainty and incomplete information - Legal reasoning with vague notions - Defeasible normative systems - Implementations and applications in the legal domain - Large-scale normative reasoning *Important Dates* - Paper submission: Jul 31st, 2018 - Notification to authors: November 30th, 2018 - Camera-ready: January 1st, 2019 *Submission Instructions* Papers submitted to the special issue must be sent to Jane Spurr (jane.sp...@kcl.ac.uk). Please specify this special issue in the email subject. We expect papers of about 15-30 pages; however, justified exceptions are possible. Each submission will be assigned with two reviewers. If have any enquiries/comments, please contact Livio Robaldo at: livio.roba...@uni.lu -- Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
