[Hol-info] Call for Workshop Proposals: International Conference on Logic Programming and Nonmonotonic Reasoning, Espoo, Finland, July 3-6, 2017
Call for Workshop Proposals 14th International Conference on Logic Programming and Nonmonotonic Reasoning Espoo, Finland, July 3 - 6, 2017 URL: http://lpnmr2017.aalto.fi The 14th International Conference on Logic Programming and Nonmonotonic Reasoning will be held in Espoo, Finland from July 3 to 6, 2017. LPNMR is a forum for exchanging ideas on declarative logic programming, non-monotonic reasoning, and knowledge representation. Workshops collocated with LPNMR are one of the best venues for the presentation and discussion of preliminary work, novel ideas, and new open problems regarding the topics of LPNMR, which include, but not limited to: 1. Foundations of LPNMR Systems: * Semantics of new and existing languages; * Action languages, causality; * Formalization of Commonsense Reasoning and understanding its laws and nature; * Relationships among formalisms; * Complexity and expressive power; * Inference algorithms and heuristics for LPNMR systems; * Extensions of traditional LPNMR languages such as new logical connectives or new inference capabilities; * Updates, revision, and other operations on LPNMR systems; * Uncertainty in LPNMR systems. 2. Implementation of LPNMR systems: * System descriptions, comparisons, evaluations; * Algorithms and novel techniques for efficient evaluation; * LPNMR benchmarks. 3. Applications of LPNMR: * Use of LPNMR in Commonsense Reasoning and other areas of KR; * LPNMR languages and algorithms in planning, diagnosis, argumentation, reasoning with preferences, decision-making, and policies; * Applications of LPNMR languages in data integration and exchange systems, software engineering and model checking; * Applications of LPNMR to bioinformatics, linguistics, psychology, and other sciences; * Integration of LPNMR systems with other computational paradigms; * Embedded LPNMR: Systems using LPNMR subsystems. Collocated workshops also provide an opportunity for presenting specialized topics and opportunities for intensive discussions and project collaboration. The format of the workshop will be decided by the workshop organizers, but ample time should be allowed for general discussion. Workshops can vary in length, but the optimal duration will be half a day or a full day. We expect the workshops to be on July 3, 2017. Workshop Proposal: == Those interested in organizing a workshop at LPNMR 2017 are invited to submit a workshop proposal. Proposals should be in English and about 1-2 pages in length. They should contain: * The title of the workshop * A brief technical description of the topics covered by the workshop * A discussion of the timeline and relevance of the workshop * A list of some related workshops held in the recent years * An estimate of the number of expected attendees * The names, affiliation, and contact details (email, web page) of the workshop organizer(s) together with a designated contact person * The previous experience of the workshop organizing committee in workshop/conference organization Proposals are expected in ASCII or PDF format. All proposals should be submitted to the Workshop Chair (Joohyung Lee, joo...@asu.edu) by email no later than December 20, 2016. Reviewing Process: == Each submitted proposal will be reviewed by the Workshop Chair and the Conference Program Chairs. Proposals that appear well-organized and that fit the goals and the scope of LPNMR will be selected. The decision will be notified by email to the responsible organizer by December 27, 2016. Workshop Organizers' Tasks: === * Producing a "Call for Papers" for the workshop and posting it on the Internet and other means * Providing a brief description of the workshop for the conference program * Reviewing/accepting submitted papers * Scheduling workshop activities in collaboration with the local organizers and the Workshop Chair * Sending workshop program and workshop proceedings in pdf format to the Workshop Chair for distribution at the conference (Apologies if you receive multiple copies of this email. Please distribute to interested parties.) -- ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] 1st CFP: IMBSA 2017 - International Symposium on Model-Based Safety and Assessment
= IMBSA 2017 International Symposium on Model-Based Safety and Assessment Trento, Italy, 11-13 September 2017 First Call for Papers = The 5th International Symposium on Model Based Safety and Assessment (IMBSA 2017) will be held in Trento, Italy. IMBSA is the key event in the field of MBSA bringing together the latest developments in model-based engineering, formal techniques, probabilistic analyses and cutting edge optimisation to address hard problems in the design of safe complex systems including software intensive and open cyber-physical systems. The symposium provides a dedicated forum, where state-of-the-art research, leading edge technology and industrial experiences are brought together. The objectives are to present experiences and tools, to share ideas, and to consolidate and grow the community. IMBSA solicits two types of contributions: - Regular submissions should present significant (theoretical or practical) novel results to the model-based safety assessment community, and discuss advances with respect to the state-of-the-art. Possible contributions include, but are not limited to: research papers focusing on the theoretical foundations or implementation of model-based technology; case study papers reporting on industrial-size applications of these methods; tool papers focusing on the theoretical foundations, design, implementation and usage of model-based tools; industrial experience papers reporting on practical use of model-based methodology and technology in industry. Regular submissions can have a maximum of 15 pages in LNCS style, and they will be presented orally at the conference. - Short submissions may report on ongoing research work, industrial applications and experiences, describe tools and their usage and/or introduce tool demonstrations. Short submissions should aim at introducing new, usable methods and tools to the model-based safety assessment community, raise new challenges and/or evaluate existing approaches on the basis of practical experiences. Short submissions can have a maximum of 2 pages in LNCS style and they will be presented either orally or as a poster/demo at the conference, at discretion of the Program Committee. All the authors of accepted tool papers and demonstrations, will be given the opportunity to present their tools live in an interactive session. Topics of Interest We solicit contributions concerning the design and verification of of safety critical systems and applications using model-based methods. Conference topics include, but are not limited to: - System Dependability Modeling and Assessment - Domain Specific Modeling Formalisms - Model-Driven Engineering Methodologies - Specification, Traceability and Verification of Safety Requirements - System Architecture and Optimization - System Engineering Modeling Tools with Safety Assessment Capabilities - Certification and Standardization of and with Model-Based Methods - Integration in Interdisciplinary Processes - mod...@run.time - Case Studies and Practical Experiences The IMBSA Approach IMBSA is looking back at a rich tradition of successfully combining research with a high number of industrial contributions. It shows that bridging the gap between basic research and industrial practice can be done effectively through interactive presentation of tools and methods. To take this into account, the conference will - in contrast to solely scientific events - be split into three main parts: - A scientific part, where newest findings are presented by renown scientists - A tools and tutorials parts, in which consolidated research achievements are interactively demonstrated - One part reporting on experiences and hot challenges in industrial practice of safety critical systems This way, participants from the industry learn about new tools and techniques, while research groups and spin-off companies can present their achievements to an interested audience. Also industrial contributors and young spin-offs can convince future customers of their tools in this mixed environment. We believe, that this mixture of conventional talks about newest achievements, presentation of practical experiences and interactive learning allows for fruitful discussions, exchange of information as well as future cooperation. Submission Details For each contribution, an abstract should be submitted by 31 January 2017, using the EasyChair website, whereas full papers must be submitted by 28 February 2017. Regular submissions should not exceed 15 pages, whereas short submissions are limited to 2 pages. Both forms of submission have to comply with the LNCS style format. All papers will be subjected to a full review by the Program Committee. It is planned to publish regular contributions as a proceedings volume. To be considered for the proceedings, at
[Hol-info] PostDoc Positions on Planning and Scheduling in the Embedded System Research Unit
(We apologize if you receive multiple copies of this message) == Call ES_PANDS_2017_postdoc == Opening date: December 1, 2016 Closing date: January 16, 2017 A PostDoc position is available in the Embedded Systems Research Unit (ES) at Bruno Kessler Foundation (FBK), Center for Information Technology. FBK is a private research institution based in Trento (Italy) and operating in different scientific fields and disciplines. As such, it has the role of keeping the Autonomous Province of Trento within the mainstream of international research. FBK is made up of seven research centers, whose activities and production are available at http://www.fbk.eu/research-centers. The Embedded Systems Research Unit (ES Unit) of the Information and Communication Technology Center of the Bruno Kessler Foundation (FBK-irst), Trento, Italy consists of about 25 people, including researchers, post-docs, PhD students, Master Students, and programmers. The Unit carries out basic and applied research, tool development and technology transfer in the field of automated planning for different application contexts, and design and verification of embedded systems. Current research directions include: * Model based planning and scheduling for aerospace systems, for the management of autonomous vehicles, for factory automation, and for process optimizations (with applications in Industry 4.0), leveraging model checking and satisfiability modulo theory techniques; * Formal Requirements Analysis based on techniques for temporal logics (consistency checking, vacuity detection, input determinism, cause-effect analysis, realizability and synthesis); * Model-based engineering and formal verification of aerospace systems using model checking techniques; * Model based on-board reasoning systems for autonomous vehicles using planning and scheduling techniques; * Formal Safety Analysis, based on the integration of traditional (e.g. Fault-tree analysis, FMEA) with symbolic verification techniques. * Model based techniques for fault detection, identification relying on model checking techniques; * Model based recovery relying on planning and scheduling techniques; * Satisfiability Modulo Theory, and its application to planning and scheduling, verification of hardware, embedded critical software, and hybrid systems (Verilog, SystemC, C/C++, StateFlow/Simulink); More information about the ES Unit is available at http://es.fbk.eu/ . == Job Description == The ES Unit has an opening for a PostDoc position in the field of planning and scheduling for industrial applications in the framework of several research and technology transfer projects. The successful candidate will be employed for a period of at least two years (with a trial period of 6 months). He/She will carry out research activities in the field of planning and scheduling and architectures for autonomy (planning, scheduling, execution, monitoring) applied to the design and implementation of adaptive systems with critical timing, safety and security requirements. In particular, the activities will focus on: * declarative languages to specify planning and scheduling domains, keeping into account controllability, partial observability, timing, and resources issues; * declarative languages to specify conditional time triggered plans suitable to solve complex planning and scheduling problems; * design and implementation of scalable planning and scheduling solution techniques for applications in industrial settings to control autonomous vehicles as well as for factory automation; * design and implementation of formal validation techniques for validation of planning and scheduling domains, and for the verification of conditional time triggered plans; * design and implementation of autonomy architectures encompassing, deliberation, execution and monitoring and interface with low level controls. The candidate is expected to work in collaboration with other researchers, programmers, and students involved in the project. Required: * PhD in computer science, mathematics or electronic engineering (to be completed within 2017); * Software development skills (preferably in C, C++, Python or Java); * Ability to carry out an independent research program; * Ability to work in a collaborative environment and deliver in research projects and possibly in industrial projects; * Oral and written proficiency in English; Preferred: In depth previous experience in at least one of the following areas: * Planning and Scheduling * Autonomy Architecture * Symbolic Model Checking * Solid background in logic * Temporal Logics and Property Specification Languages * Satisfiability
[Hol-info] WiL 2017: Women in Logic Workshop Call for Papers
Call for Papers WiL 2017: Women in Logic Workshop Reykjavik, Iceland June 19, 2017 https://sites.google.com/site/firstwomeninlogicworkshop/ Affiliated with the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 20-23 June 2017, Reykjavik, Iceland. We are holding the first Women in Logic (WiL) workshop as a LICS associated workshop this year. The workshop intends to follow the pattern of meetings such as Women in Machine Learning (WiML, http://wimlworkshop.org/) or Women in Engineering (WIE, (http://www.ieee-ras.org/membership/women-in-engineering) that have been taking place for quite a few years. Women are chronically underrepresented in the LICS community; consequently they sometimes feel both conspicuous and isolated, and hence there is a risk that the under-representation is self-perpetuating. The workshop will provide an opportunity for women in the field to increase awareness of one another and one another's work, to combat the feeling of isolation. It will also provide an environment where women can present to an audience comprised of mostly women, replicating the experience that most men have at most LICS meetings, and lowering the stress of the occasion; we hope that this will be particularly attractive to early-career women. Topics of interest of this workshop include but are not limited to the usual Logic in Computer Science (LICS) topics. These are listed as automata theory, automated deduction, categorical models and logics, concurrency and distributed computation, constraint programming, constructive mathematics, database theory, decision procedures, description logics, domain theory, finite model theory, formal aspects of program analysis, formal methods, foundations of computability, higher-order logic, lambda and combinatory calculi, linear logic, logic in artificial intelligence, logic programming, logical aspects of bioinformatics, logical aspects of computational complexity, logical aspects of quantum computation, logical frameworks, logics of programs, modal and temporal logics, model checking, probabilistic systems, process calculi, programming language semantics, proof theory, real-time systems, reasoning about security and privacy, rewriting, type systems and type theory, and verification. SUBMISSIONS Contributions should be written in English and submitted in the form of full papers (with a maximum of 10 pages) or short papers (with a maximum of 5 pages). They must be unpublished and not submitted simultaneously for publication elsewhere. The papers should be prepared in latex using the LICS style (IEEE Proceedings 2-column 10pt). LaTeX style files are available at http://www.ctan.org/tex-archive/macros/latex/contrib/IEEEtran/. Please use IEEEtran.cls version V1.8b, released on 26/08/2015. The submission should be in the form of a PDF file uploaded to the WiL 2017 Easychair page (https://easychair.org/conferences/?conf=wil2017) before the submission deadline of February 17th, 2017, anywhere on Earth. PROCEEDINGS We plan to publish a post conference volume at ENTCS or other equally visible outlet. IMPORTANT DATES Paper submission deadline: February 17th, 2017 Author notification: March 15th, 2017 Contribution for Proceedings: 15 April 2017 Final program: 1 May 2017 INVITED SPEAKERS * Claudia Nalon (University of Brasilia, Brasil) * Catuscia Palamidessi (INRIA Saclay and LIX, France) SCIENTIFIC AND ORGANIZING COMMITTEE * Valeria de Paiva (Chair, Nuance Communications, USA) * Adriana Compagnoni (Stevens Institute of Technology, USA) * Amy Felty (University of Ottawa, Canada) * Anna Ingolfsdottir (Reykjavik University, Iceland) * Ursula Martin (University of Oxford, UK) * Brigitte Pientka (McGill University, Canada) * Alexandra Silva (University College London, UK) * Perdita Stevens (University of Edinburgh, UK) -- 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] Henkin's paper "Completeness in the Theory of Types" (1950); Ramsey (and Chwistek)
Dear Members of the Research Community,
Concerning Henkin's paper "Completeness in the Theory of Types" (1950), I have
a question.
Theorem 2 is claimed to be false in Andrews' newest publication that forms part
of the volume on Leon Henkin edited by Manzano et al.: "Thus, Theorem 2 of
[Henkin, 1950] (which asserts the completeness and soundness of C) is
technically incorrect. The apparently trivial soundness assertion is false."
[Andrews, 2014b, p. 70]
For an extended quote, see the very end of the section "Criticism" of
http://doi.org/10./100.111
Have there been any formalization efforts for Theorem 2 of [Henkin, 1950], such
that the above claim can be verified (or refuted) by mechanized reasoning
(formalization in a computer)?
Following a purely syntactic approach, I usually skip semantic issues, but
this nevertheless seems an interesting question to me.
According to Roger Bishop Jones's advice at
https://sourceforge.net/p/hol/mailman/message/35435344/
now Ramsey (and Chwistek) was added to the diagram at
http://doi.org/10./100.111
who first suggested the simple theory of types according to footnote 1 of
[Church, 1940],
Both Chwistek and Ramsey are mentioned in the "Introduction to the Second
Edition" of "Principia Mathematica" in some way, but I am not familiar with the
details of how strong the impact on Russell's own theory was.
In paragraph 9 of Carnap's 1929 German-language "Abriss der Logistik"
(referenced in Church's footnote 1), Ramsey is mentioned, but not Chwistek (who
is referenced indirectly through p. xiv of the Introduction to the 2nd ed. of
PM - see Carnap, pp. 21 f.).
In Quine's introduction to Russell's 1908 essay "Mathematical Logic as Based on
the Theory of Types" only Ramsey is mentioned (van Heijenoort, 1967, p. 152).
It is interesting to see that both Ramsey and Henkin ("Identity as a logical
primitive", 1975) prefer the term 'identity' rather than 'equality', which is
also my preference, as mentioned at
https://sourceforge.net/p/hol/mailman/message/35446249/
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00070.html
Ramsey: "[M]athematics does not consist of tautologies, but of [...]
'equations', for which I should prefer to substitute 'identities'. [...] [I]t
is interesting to see whether a theory of mathematics could not be constructed
with identities for its foundation. I have spent a lot of time developing such
a theory, and found that it was faced with what seemed to me insuperable
difficulties."
Quoted in: [Andrews, 2014b, p. 67]
Available online at: http://www.hist-analytic.com/Ramsey.htm
For the references, please see:
http://doi.org/10./100.111
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10./100
--
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
