text:
NEWSLETTER No. 83, April 2009
Reiner Hähnle re-elected as CADE vice-president
Call for Nominations for Herbrand Award
Call for Nominations: Editor-in-Chief of ACM Transactions on Computational Logic (ToCL)
Woody Bledsoe Student Travel Awards
Practical Progress in the Development of Automated Theorem Proving for Higher-order Logic
The Higher-order TPTP
The Typed Higher-order Form (THF) Language
Collecting THF Problems, for the TPTP
TPTP Infrastructure for THF Problems
Collecting Solutions to THF Problems, for the TSTP
Higher-Order ATP for the TPTP
LEO-II
IsabelleP and IsabelleM
RDP 2009, Fed. Conf. on Rewriting, Deduction, and Programming
CICM, Conferences on Intelligent Computer Mathematics
TABLEAUX 2009, Automated Reasoning with Analytic Tableaux and Related Methods
CADE-22: The Intl. Conference on Automated Deduction
TPHOLs, Theorem Proving in Higher-Order Logics
FroCoS'09, Frontiers of Combining Systems
The Intl. Tbilisi Symposium on Language, Logic and Computation
FTP 2009, the Workshop on First-Order Theorem Proving
VLL, Workshop on Visual Languages and Logic
Special Issue of Studia Logica: The Contributions of Logic to the Foundations of Physics
System Announcement: the ProofWeb system
Book Announcement: Handbook of Practical Logic and Automated Reasoning
Many areas of logic can be studied successfully with an automated reasoning program. Equivalential calculus, classical propositional calculus, and others are such. Indeed, reasoning programs have occasionally played a key role in answering open questions in logic. Here you are offered a challenge.
An automated reasoning program can sometimes be used to show that no proof exists, where the argument does not depend on finding an appropriate model. For example, in the early 1980s, certain formulas in equivalential calculus were shown to be too weak, by characterizing all of the deducible formulas from each and showing that certain theorems could, therefore, not be deduced. From the viewpoint of logic, knowing that a formula cannot serve as a single axiom is often as interesting as knowing that it can.
Let's consider the axioms of the BCI logic.
P(i(i(x,y),i(i(z,x),i(z,y)))).  % B
P(i(i(x,i(y,z)),i(y,i(x,z)))).  % C
P(i(x,x)).                      % I
Condensed detachment is a typical rule of inference used to study such systems. It is captured by the following in the presence of hyperresolution.
-P(i(x,y)) | -P(x) | P(y).  %  condensed detachment
And here is a candidate formula that I find enticing.
P(i(u,i(i(v,w),i(i(i(x,x),i(y,i(u,v))),i(y,w))))). % BCI-Candidate 42
You are asked to formulate, if possible, an automated method showing that Candidate 42 is not a single axiom. It is, in fact, a theorem of BCI, but so far I have been unable to show that it is strong enough to be a single axiom. I doubt it is, my suspicion being based on the fact that, as it appears, all deducible theorems from the formula contain an alphabetic variant of i(x,x). But I would love to be proved wrong.
Here's another candidate formula presenting a challenge of a different type.
P(i(i(i(i(i(u,u),i(v,w)),i(i(x,v),w)),y),i(x,y))). % BCI-Candidate 46
I've included Candidate 46 in that its use as the sole hypothesis in the BCI logic seems somewhat promising, for it leads to theorems that are interesting. Yet I have not been able to prove its status as a single axiom.
Lest you be discouraged, let me assure you that I and a few of my colleagues have played with other candidate formulas that, after considerable effort, turned out to be single axioms.
Perhaps you will prove something of interest for the forthcoming CADE-22 conference, which focuses on logics and proofs.
Wolfgang Ahrendt
E-mail: ahrendt (at) chalmers.se
An election was held from November 4 through Noveber 25 to fill two positions on the board of trustees of CADE Inc. Alessandro Armando, Christoph Benzmüller, Reiner Hähnle, Konstantin Korovin, Brigitte Pientka, and Cesare Tinelli were nominated for these positions. (See AAR Newsletter No. 82, November 2008.)
Ballots were sent by electronic mail to all members of AAR on November 4, for a total of 773 ballots. Of these, 139 were returned with a vote, representing a participation level of 18% (as compared to 16.4% in 2007, 16.0% in 2006, 18.1% in 2005 and 19.8% in 2004 and 2003). All votes were valid. Therefore, in each iteration of the STV algorithm (the STV (Single Transferrable Vote) algorithm is described in the CADE Bylaws), a candidate is elected iff he or she gets strictly more than 69 1st preference votes. Otherwise, the votes of the candidate with the least 1st preference votes are redistributed.
Candidate 1st pref. 2nd pref. 3rd pref. 4th pref. 5th pref. 6rd pref. Total
A.Armando 20 14 20 20 12 53 139
C.Benzmüller 26 29 16 9 11 48 139
R.Hähnle 38 19 14 12 9 47 139
K.Korovin 12 17 9 7 12 82 139
B.Pientka 24 20 23 8 10 54 139
C.Tinelli 19 30 20 12 7 51 139
No candidate reaches more than 69 1st preference votes. By redistributing the votes of K.Korovin one gets the following table:
C.Benzmüller 31 27 15 12 27 27 139
R.Hähnle 39 20 14 16 25 25 139
B.Pientka 26 22 23 10 26 32 139
C.Tinelli 20 37 14 15 24 29 139
No candidate reaches more than 69 1st preference votes. By redistributing the votes of C.Tinelli one gets the following table:
No candidate reaches more than 69 1st preference votes. By redistributing the votes of A.Armando one gets the following table:
C.Benzmüller 42 33 25 16 18 5 139
B.Pientka 37 31 26 17 19 9 139
No candidate reaches more than 69 1st preference votes. By redistributing the votes of B.Pientka one gets the following table:
R.Hähnle 63 35 10 15 12 4 139
No candidate reaches more than 69 1st preference votes. By redistributing the votes of C.Benzmüller one gets the following table:
R.Hähnle 98 1 16 15 9 0 139
Now, R.Hähnle reaches more than 69 1st preference votes, and is elected to the board of trustees. The redistribution of his votes produces the following table:
K.Korovin 15 17 13 11 58 25 139
C.Benzmüller 60 37 7 22 13 0 139
C.Tinelli 58 39 6 16 16 4 139
C.Benzmüller 97 1 19 16 6 0 139
Now, C.Benzmüller reaches more than 69 1st preference votes, and is elected to the board of trustees.
Altogether, the two candidates who are elected to the board of trustees in this election are Reiner Hähnle and Christoph Benzmüller.
After this election, the following people (listed alphabetically) are serving on the board of trustees of CADE Inc.:
Wolfgang Ahrendt (Secretary, appointed 5/2007)
Franz Baader (President, CADE-19 Program Chair, elected 10/2003, reelected 10/2006)
Peter Baumgartner (elected 10/2003, reelected 10/2006)
Christoph Benzmüller (elected 11/2008)
Maria Paola Bonacina (Secretary 9/1999 to 5/2004, elected 10/2004, reelected 10/2007)
Amy Felty (Secretary 5/2004 to 5/2007, elected 10/2007)
Reiner Hähnle (Vice President, elected 10/2005, reelected 11/2008)
Neil Murray (Treasurer)
Renate Schmidt (CADE-22 program chair)
Geoff Sutcliffe (elected 10/2004, reelected 10/2007)
Aaron Stump (elected 10/2006)
Andrei Voronkov (CADE-18 Program Chair, elected 10/2002, Vice President 2003, elected 10/2007)
On behalf of the AAR and CADE Inc., I thank Cesare Tinelli for his service as trustee during the past 3 years, Alessandro Armando for his service as ex-officio trustee (as IJCAR 2008 program co-chair), all candidates for running in the election, all the members who voted; and offer congratulations to Reiner Hähnle and Christoph Benzmüller on being elected.
The newly formed board of trustees held an election of the CADE vice-president, as the term of Reiner Hähnle as vice-president was expiring. Reiner was re-nominated, and furthermore, Maria Paola Bonacina was nominated. Out of these two, Reiner was elected. We thank Maria Paola and Reiner for running in the election, and offer congratulations to Reiner for being re-elected.
Harald Ganzinger (2004)
Martin Davis (2005)
Wolfgang Bibel (2006)
Alan Bundy (2007)
Edmund Clarke (2008)
A nomination is required for consideration for the Herbrand award. The deadline for nominations for the Herbrand Award that will be given at CADE 2009 is May 12, 2009.
Nominations pending from previous years must be resubmitted in order to be considered. Nominations should consist of a letter (preferably email) of up to 2,000 words from the principal nominator, describing the nominee's contribution, along with letters of up to 2,000 words of endorsement from two other seconders. Nominations should be sent to Franz Baader, president of CADE Inc. (baader (at) tcs.inf.tu-dresden.de) with copies to Wolfgang Ahrendt (ahrendt (at) chalmers.se).
Nominations (including self nominations) are invited for the next Editor-in-Chief of ACM Transactions on Computational Logic (ToCL), see here. The position is for a term (renewable once) of three years, starting on July 1, 2009.
Candidates should be well-established researchers in areas related to computational logic, broadly conceived, and should have sufficient experience serving on conference program committees and journal editorial boards. Nominations, including a current curriculum vita and a brief (one page) statement of vision for ToCL, should be sent to Joseph Halpern , by May 1, 2009.
Final selection will be made by a Selection Committee, consisting of Joseph Halpern (chair – Cornell University), Kryzsztof Apt (CWI), Prakash Panangaden (McGill University), and Gordon Plotkin (University of Edinburgh). Nominations received after May 1, 2009, will be considered up until the position is filled.
The Woody Bledsoe Student Travel Award is intended to enable selected students to attend the the Conference on Automated Deduction (CADE) by covering much of their expenses. The winners of the travel award will be (partially) reimbursed for their conference registration, transportation, and accommodation expenses (past awards have varied, but have typically been corresponding to CA$250 to CA$1000). Preference will be given to students who will play an active role in the conference, including satellite workshops, and do not have alternative funding. However, also students in other situations are very much encouraged to apply.
The awards are sponsored by CADE Inc.
See the CADE 2009 web pages for more information, including application details. The deadline for applications is 16 June 2009.
Geoff Sutcliffe** and Chris Benzmüller
with help from lots of people, particularly
Chad Brown and Frank Theiss*** and Florian Rabe,
and with honorable mention
Lucas Dixon, Stefan Berghofer, Makarius Wenzel, Jasmin Blanchette, Andrei Tchaltsev, Alexandre Riazanov.
* The research leading to these results has received funding from the European Community's Seventh Framework Programme FP7/2007-2013, under grant agreement PIIF-GA-2008-219982.
** Most of the work was done while hosted as a guest of the Automation of Logic group in the Max Planck Institut für Informatik.
*** Supported by the German Federal Ministry of Education and Research (BMBF) in the framework of the Verisoft XT project under grant 01 IS 07 008.
There is a well established infrastructure that supports research, development, and deployment of first-order Automated Theorem Proving (ATP) systems, stemming from the Thousands of Problems for Theorem Provers (TPTP) problem library. This infrastructure has been central to the progress that has been made in the development of high performance first-order ATP systems. Until recently there has been no corresponding support in higher-order logic. In 2008, work commenced on extending the TPTP to include problems in higher-order logic, and developing the corresponding infrastructure and resources. These efforts aim to have an analogous impact on the development of higher-order ATP systems. This is a description of the practical progress that has been made towards this goal.
The TPTP language is a human-readable, easily machine-parsable, flexible and extensible language, suitable for writing both ATP problems and solutions. A particular feature of the TPTP language, which has been maintained in the THF part, is Prolog compatibility. The THF language for logical formulae is a syntactically conservative extension of the existing first-order TPTP language, adding constructs for higher-order logic. The THF language has been divided into three layers: THF0, THF, and THFX. The THF0 core language is based on Church's simple type theory, and provides the commonly used and accepted aspects of a higher-order logic language. The full THF language drops the differentiation between terms and types, thus providing a significantly richer type system, and adds the ability to reason about types. It additionally offers more term constructs, more type constructs, and more connectives. The extended THFX language adds constructs that are "syntactic sugar", but are usefully expressive.
Here is an example of a TPTP problem file in THF0. The constructs that are not part of the first-order TPTP language are:
The typing of constants and quantified variables. THF requires that all symbols be typed. Constants are globally typed in an annotated formula with role type, and variables are locally typed in their quantification (thus requiring all variables to be quantified).
$tType for the collection of all types.
$i and $o for the types of individuals and propositions. $i is non-empty, and may be finite or infinite.
> (right associative) type mapping.
^ as the lambda binder.
@ for (left associative) application.
Additional THF constructs, not shown in the example, are:
The use of connectives as terms (THF0).
!! and ?? for the π (forall) and σ (exists) operators (THF0).
!> and ?* for Π (dependent product) and Σ (dependent sum) types (THF).
[ ] for tuples (THF).
* and + as cross product and union type constructors (THF).
:= as a connective for global definitions, and as a binder and separator for local definitions (ala letrec) (THFX).
--> as the sequent connective (THFX).
TPTP v3.7.0 was released in March 2009. This was a beta release of the THF part of the TPTP, and contained higher-order problems in only the THF0 language. There were 1275 THF problem versions, stemming from 852 abstract problems, in ten domains:
ALG - 50 problems. These are problems concerning higher-order abstract syntax, encoded in higher-order logic.
GRA - 93 problems. These are problems about Ramsey numbers, some of which are open in the mathematics community.
LCL - 61 problems. These are of modal logic problems that have been encoded in higher-order logic.
NUM - 221 problems. These are mostly theorems from Jutting's AUTOMATH formalization of the well known Landau book. There are also some Church numeral problems.
PUZ - 5 problems. These are "knights and knaves" problems.
SET and SEU - 749 problems. Many of these are "standard" problems in set theory. Many have TPTP versions in first-order logic, which allows for an evaluation of the relative benefits of the different encodings with respect to ATP systems for the logics. There is also a significant group of problems in dependently typed set theory, and a group of interesting problems about binary relations.
SWV - 37 problems. The two main groups of problems are (i) security problems in access control logic, initially encoded in modal logic, and subsequently encoded in higher-order logic, and (ii) problems about security in an authorization logic that can be converted via modal logic to higher-order logic.
SYN and SYO - 59 problems. These are simple problems to test properties of higher-order ATP systems.
1002 of the problems (78%) contain equality. 1166 of the problems (92%) are known or believed to be theorems, 26 (2%) are known or believed to be non-theorems, 4 (0%) are are known or believed to be unsatisfiable sets of formulae, 3 (0%) are are known or believed to be satisfiable sets of formulae, 68 (5%) are open, and the remaining 8 problems (0%) have unknown status. These problems can be downloaded as part of TPTP v3.7.0 from the TPTP web site, or browsed online. Many more problems are expected by the time TPTP v4.0.0 is released in August 2009.
From a TPTP user perspective, the TPTP2X utility distributed with the TPTP will initially be most useful for manipulating THF problems. TPTP2X has been extended to read, manipulate, and output (pretty print) data in the full THF language. Additionally, format modules for outputting problems in the TPS, Twelf, OmDoc, and Isabelle formats have been implemented. The TPTP4X tool has also been extended to read, manipulate, and output data in the THF0 language, and will be extended to the full THF language in 2009.
The SystemOnTPTP interface for running ATP systems and tools on TPTP problems and solutions has been updated to deal with THF data, including use of the new higher-order formats output by TPTP2X.
Internally, an important resource is the Twelf-based type checking of THF problems, implemented by exporting a problem in Twelf format, and submitting the result to the Twelf tool. The BNF based parsers for the TPTP naturally parse the full THF language, and the lex/yacc files used to build these parsers are freely available.
The Thousands of Solutions from Theorem Provers (TSTP) solution library, the "flip side" of the TPTP, is a corpus of contemporary ATP systems' solutions to the TPTP problems. Three higher-order ATP systems, LEO-II 0.99a, TPS 3.0, and two automated versions of Isabelle 2008 (one - IsabelleP - trying to prove theorems, the other - IsabelleM - trying to find (counter-)models), have been run over the 1275 THF problems in TPTP v3.7.0, and their results added to the TSTP. The systems are described below. This table tabulates the numbers of problems solved. The results show that the GRA Ramsey number problems are very difficult - this was expected. For the remaining domains the problems pose interesting challenges for the ATP systems, are the differences between the systems lead to different problems being solved, including some that are solved uniquely by each of the systems.
PUZ
SE?
SY?
Problems 50 93 61 221 5 749 37 59 1275
THM/UNS 50 25 51 221 5 746 25 47 1170
CSA/SAT 0 0 10 0 0 3 5 11 29
LEO-II 0.99a 34 0 48 181 3 401 19 42 725 127
IsabelleP 2008 0 0 0 197 5 361 1 30 594 74
TPS 3.0 10 0 40 150 3 285 9 35 532 6
Any 32 0 50 203 5 490 20 52 843 207
All 0 0 0 134 2 214 0 22 372
None 18 93 12 18 0 259 17 15 432
IsabelleM 2008 0 0 1 0 0 0 0 8 9
Research and development of computer-supported reasoning for higher-order logic has been in progress for as long as that for first-order logic. It has become clear that the computational issues in the higher-order setting are significantly harder than those in first-order. Thus, while there are many interactive proof assistants based on some form of higher-order logic, there are few automated systems for higher-order logic. The three (fully automatic) higher-order ATP systems that we know of are LEO-II, TPS, and IsabelleP/M. These are available for use in the SystemOnTPTP interface.
LEO-II is a resolution based higher-order ATP system. LEO-II is implemented in Objective Caml, and is freely available under a BSD like licence. LEO-II is designed to cooperate with specialist systems for fragments of higher-order logic. Currently, LEO-II is capable of cooperating with the first-order ATP systems E, SPASS, and Vampire. LEO-II directly parses THF0 input, communicates with the cooperating first-order ATP system uses TPTP standards, has been debugged using examples in the TPTP library, and will soon produce THF0 output.
TPS is a higher-order theorem proving system that has been developed under the supervision of Peter B. Andrews since the 1980s. Theorems can be proven either interactively or automatically. In TPS there are flags that can be set to affect the behavior of automated search. The automated TPS used for solving THF problems uses two different collections of flags, in modes called MS98-FO-MODE and BASIC-MS04-2-MODE. As the two modes have quite different capabilities, they are run in competition parallel as a simple way of obtaining greater coverage. It was this competition parallel version of TPS that produced the 532 proofs noted in the table above.
Isabelle is a proof assistant for higher-order logic, which is normally used interactively. A fully automatic version, called IsabelleP, has been implemented using strategy scheduling of the nine automatic tactics simp, blast, auto, metis, fast, fastsimp, best, force, and meson. While it was probably never intended to use Isabelle as a fully automatic system, this simple automation provides useful capability. The ability of Isabelle to find (counter-)models using the refute tactic has also been integrated into an automatic system, called IsabelleM.
The first THF division of CASC is being organized, and will be part of CASC-22 at CADE-22.
The core work of collecting THF problems is proceeding.
Problems in the full THF and THFX languages are being collected, and TPTP infrastructure for processing these problems is being developed.
The Java parser for the TPTP language is being extended to read the THF language.
Users are being identified.
Users and developers of ATP for higher-order logic are encouraged to submit higher-order problems to the TPTP, and to enter systems into CASC-22. Questions, suggestions, and contributions should be sent to Geoff Sutcliffe.
The Federated conference on Rewriting, Deduction, and Programming will take place on June 28 to July 03, 2009, in Brasília, Brazil.
It consists of two main events:
RTA'09, the conference on Rewriting Techniques and Applications.
TLCA'09, the conference on Typed Lambda Calculi and Applications.
There are a number of collocated events, namely:
ISR'09, the Intl. School on Rewriting
HOR'09, the Intl. Workshop on Higher-Order Rewriting
LSFA'09, the Workshop on Logical and Semantic Frameworks, with Applications
RULE'09, the International Workshop on Rule-Based Programming
WFLP'09, the Workshop on Functional and (Constraint) Logic Programming
WRS'09, the Workshop on Reduction Strategies in Rewriting and Programming
IFIP WG 1.6, the IFIP Working Group 1.6 meeting
Early registration closes on May 1.
See the conference web page for full details!
This is a federated conference that will take place on July 6–12, 2009 in Ontario, Canada.
It consists of two conferences:
Calculemus 2009, the Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, July 6–7. Calculemus is dedicated to the integration of computer algebra systems and systems for mechanised reasoning, interactive theorem provers or proof assistants, and automated theorem provers.
For short papers on emerging trends, the abstract submission deadline is April 30, and the submission deadline May 7, 2009.
MKM 2009, the Intl. Conf. on Mathematical Knowledge Management, July 10–12.
Additionally, there will be the following workshops:
CCA, Compact Computer Algebra, 10 July - 11 July
DML, Towards a Digital Mathematics Library, 7 July - 9 July
MathUI Mathematical User Interfaces, 6 July
OpenMath Workshop on OpenMath, 9 July
Pen-Math Pen-Based Mathematical Computation, 8 July - 9 July
See the conference web page for full details on all events.
The next International Conference on Automated Reasoning with Analytic Tableaux and Related Methods will take place in Oslo, Norway, July 6–10, 2009.
TABLEAUX 2009 will be collocated with FTP 2009.
There will be three smaller workshops on July 6:
Tableaux versus automata as logical decision methods, organised by Valentin Goranko (Univ. of the Witwatersrand, Johannesburg, South Africa), see the workshop web page for details.
Proofs and Refutations in Non-Classical Logics, organised by Roy Dyckhoff (Univ. of St Andrews, Scotland) and Didier Galmiche (LORIA, Henri Poincaré Univ., Nancy, France), see the workshop web page for details.
Genzen Systems and Beyond, organised by Kai Brünnler (Univ. of Bern, Switzerland) and George Metcalfe (Vanderbilt Univ., Nashville, USA), see the workshop web page for details.
Submission to all three workshops is still possible.
Two tutorials will be part of the Tableaux programme:
The Theory of Canonical Systems, given by Arnon Avron and Anna Zamansky from Tel-Aviv University, Israel.
LoTREC: Theory and Practice. Proving by Tableau becomes easier, given by Bilal Said and Olivier Gasquet from Université Paul Sabatier in Toulouse, France.
Registration will open soon, early registration will be possible until June 5.
For full details about this event, please refer to the conference web pages
This year's International Conference on Automated Deductions will be hosted by McGill University, Montreal, Canada August 2–7, 2009.
CADE is the major forum for the presentation of research in all aspects of automated deduction.
The following subsidiary events will be part of CADE this year:
Automated Deduction: Decidability, Complexity, Tractability (ADDCT)
Beyond SAT: What About First-Order Logic?
Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)
Modules and Libraries for Proof Assistants (MLPA)
Proof Search in Type Theories (PSTT)
Satisfiability Modulo Theories (SMT)
The International Workshop on Unification (UNIF)
TPTP World Workshop (TPTPWoWo)
Hierarchical and Modular Reasoning in Complex Theories
Probabilistic Analysis Using a Theorem Prover
(Challenges and Solutions for) Precise, Automated and Scalable Verification of Systems Software Using SMT solvers
Logics with undefinedness: How to modify a traditional logic so that it handles undefinedness in accordance with mathematical practice
System competitions:
The CADE ATP System Competition (CASC)
Satisfiability Modulo Theories Competition (SMT-COMP)
Submission to all workshops is still possible!
Registration will open around May 20. The deadline for early registration is June 30.
See here for full details on this conference.
The 22th International Conference on Theorem Proving in Higher Order Logics, TPHOLs, will take place on August 17–20, 2009 in Munich, Germany.
TPHOLs is a series of international conferences that brings together researchers working in all areas of interactive theorem proving, higher-order logics, and related topics.
The following workshops will be collocated with TPHOLs:
PLMMS, Programming Languages for Mechanized Mathematics Systems (21 August)
Coq Workshop (21 August)
Isabelle Developers Workshop (13 - 15 August)
This symposium well take place in Trento, Italy, on September 16–18th, 2009.
FroCoS wants to offer a common forum for research activities in the general area of combination, modularization and integration of systems (with emphasis on logic-based ones), and of their practical use. Topics of interest include (but are not limited to):
combinations of logics such as combined predicate, temporal, modal, or epistemic logics;
combinations and modularity in ontologies;
combination of decision procedures, of satisfiability procedures, and of CS techniques;
combinations and modularity in term rewriting;
integration of equational and other theories into deductive systems;
combination of deduction systems and computer algebra;
integration of data structures into CLP formalisms and deduction processes;
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.
Proceedings will be published in the Springer LNAI series.
Abstract submission deadline: April 26th, 2009
Full paper submission deadline: May 3rd, 2009
See the conference web page for further details.
This symposium will take place in Bakuriani, Georgia, September 21–25, 2009.
The program committee invites submissions of two page abstracts on all aspects of language, logic and computation. Work of an interdisciplinary nature is particularly welcome. Areas of interest include, but are not limited to:
Natural language syntax, semantics, and pragmatics
Constructive, modal and algebraic logic
Linguistic typology and semantic universals
Logics for artificial intelligence
Information retrieval, query answer systems
Logic, games, and formal pragmatics
Language evolution and learnability
Computational social choice
Historical linguistics, history of logic
The submission deadline is May 1, 2009 ; notification is due June 15. Accepted submissions will appear in the conference proceedings. The proceedings of the Six and Seventh International Tbilisi Symposium have been published in the LNAI series with Springer.
See the conference web page for details.
This years FTP workshop will take place in Oslo, Norway, July 6–7, 2009. FTP be collocated with the Tableaux conference.
The workshop welcomes original contributions on theorem proving in first-order classical, many-valued, modal and description logics, including (but not restricted to):
theorem proving in first-order classical, many-valued, and modal logics, including:
satisfiability in propositional logic,
satisfiability modulo theories,
specialized decision procedures,
constraint reasoning,
equational reasoning,
term rewriting,
paramodulation/superposition;
strategies and complexity of theorem proving procedures;
implementation techniques;
applications of first-order theorem provers to:
program verification,
model checking,
artificial intelligence,
computational linguistics.
The deadline for paper submissions is April 20.
Accepted submissions will be published as a technical report of the University of Oslo. They will also be available on the web. As for the previous editions of FTP, a journal special issue is planned after the workshop.
Check the workshop web page for further details.
This workshop will take place In Corvallis, Oregon, US, on September 20, 2009.
The purpose of the VLL workshop is to explore the current state of research at the intersection of logic and visual languages, examining notations or software in which a graphical structure provides the foundation for, or a visualisation of, a system of logic. Topics of interest include, but are not limited to:
Graphical notations for logics (either classical or non-classical, such as first or higher order logic, temporal logic, description logic, independence friendly logic, spatial logic)
Diagrammatic reasoning
Formalisation (syntax, semantics, reasoning rules)
Expressiveness of visual logics
Visual logic programming languages
Visual specification languages
Tool support for Visual Logics
The submission deadline is June 22, 2009.
See the event's web page for full details.
The special issue specifically, though not exclusively, invites contributions on the following topics:
The use of techniques originating from classical logic, modal logic and multi-dimensional modal logics, spatial logic, dynamic logic, temporal logic, epistemic logic, linear logic and other resource-sensitive logics, intuitionistic logic, game logics, process algebras, co-algebraic logics, categorical logics, many-valued logics, quantum logics etc. to formalize physical theories or to reason about their concepts, phenomena and/or applications.
Logical techniques used in quantum information theory, including quantum computation, quantum communication, quantum cryptography and quantum programming.
Philosophical contributions on the meaning of concepts such as truth, consequence, completeness, implication and (quantum) information viewed at the interface of Logic and Physics.
Open problems in modern physics, soliciting new techniques from logic, computation or information theory.
Explorations on how to use new formal methods in combination with insights and interpretations in the philosophy of physics to yield new perspectives on the main foundational issues and open problems in modern physics.
Answers to the questions: "What can physics learn from logic?" and/or "What can logic learn from physics?"
DEADLINE FOR SUBMISSION OF MANUSCRIPTS: May 31, 2009
The full CfP, including submission instructions is available in PDF format here
ProofWeb is a system for using proof assistants (also known as interactive theorem provers) through the web. It is taylored specifically to practising natural deduction in logic courses. The ProofWeb home page which is the entry point into the system, and which contains all relevant information about it can be found at:
http://proofweb.cs.ru.nl/
ProofWeb can be used for free, even without registration. It can be used with just a web browser, without even installing a plug-in. ProofWeb was developed to be used with the logic textbook Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan which is published by Cambridge University Press, but it also can be used in conjunction with other textbooks. ProofWeb both supports "Gentzen-style" natural deduction in which proofs are tree-like derivation, and "Fitch-style" natural deduction in which proofs are lists of lines that grouped using boxes or "flags". ProofWeb was developed for the Coq proof assistant, but has been extended to various other proof assistants. ProofWeb is already being used in several proof assistant courses and introductory logic courses.
ProofWeb has been used in prototypes for more ambitious systems, most notably in the MathWiki prototype for a Wikipedia-like system that is integrated with on-line proof assistants, and the PC-Extra calculator which can calculate numerical expressions to arbitrary precision and where the correctness of the answers is simultaneously being proved by Coq.
ProofWeb was developed in the Netherlands at the Radboud University Nijmegen and Free University Amsterdam with money from the SURF Foundation. The developer of the ProofWeb system is Cezary Kaliszyk from the Radboud University. Currently the other members of the ProofWeb team are Dan Synek, Femke van Raamsdonk, Freek Wiedijk, Herman Geuvers and James McKinna.
John Harrison
Cambridge University Press 2009, 702 pages
The sheer complexity of computer systems has meant that automated reasoning, i.e. the ability of computers to perform logical inference, has become a vital component of program construction and of programming language design. This book meets the demand for a self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. The mathematical logic foundations are described in conjunction with practical application, all with the minimum of prerequisites. The approach is constructive, concrete and algorithmic: a key feature is that methods are described with reference to actual implementations (for which code is supplied) that readers can use, modify and experiment with. This book is ideally suited for those seeking a one-stop source for the general area of automated reasoning. It can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study.
One stop reference that is broad-based and self-contained
Constructive approach that enables topics to be discussed algorithmically
Implementation of these algorithms provided as code
Can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study
For more information, see the publisher's web page.
For code and resources, see here.


text:
Brighton General Cemetery
Melbourne, Victoria, Australia
Historic Interments
Crime & Tragedy
Readers' Stories
Rev Charles Strong (1844-1942)
Published on July 28, 2019 July 28, 2019 by bgc_admin
Clergyman & Controversialist
Acknowledged as one of the most controversial clergyman in the history of the Victorian Presbyterian Church, Strong was born at Dailly, Ayrshire, Scotland on 26 September 1844 the son of Rev David Strong and Margaret née Roxburgh. While attending University of Glasgow (Hon LL.D., 1887) between 1859 and 1864 he came under the influence of Edward Caird, professor of moral philosophy and rejected the scholastic Calvinist teaching as the true and sufficient expression of the evangelical faith, instead following a more liberal theological view. Ordained in 1868, his success as a "pastor, preacher, liberal theological teacher and social reformer" led to his appointment as head of Scots Church, Collins Street (1875-83) in Melbourne. Yet, "almost from the hour of his arrival", controversy was never far away and his essays, outspoken criticism of social evils and advocacy of evangelical reform soon led to friction within the presbytery; Strong offered his resignation in August 1881 but instead agreed to take leave and he left to visit Scotland in 1882.
But his absence did little to resolve the theological divide and soon after his return he became embroiled in fresh controversy over his failure to denounce George Higinbotham's (q.v.) lecture he chaired titled "The Relation between Science and Religion" and was threatened with a libel for heresy; in a tense and dramatic sequence of events he refused to attend the General Assembly on 14 November 1883 arguing the action against him as "unconstitutional and illegal" according to the laws of the Church and defiantly set sail for Scotland the next day. In November 1884, Strong returned to Melbourne and the following year founded the Australian Church – a free religious fellowship – yet it was his controversial views that led to its eventual demise in 1957. Among the many admirers of Strong were the politician Sir James Lorimer (St. Kilda Cemetery), Alfred Felton (St. Kilda Cemetery) of "Felton, Grimwade & Co", and Alfred Deakin (St. Kilda Cemetery), thrice Prime Minister of Australia.
Residing at 7 Barnalo Grove, Armadale he died while holidaying at Lorne on 12 February 1942.
ADB Volume 6 1851-90 (R-Z).
The Age 14 February 1942.
The Herald 12 February 1942.
Macdonald, A., "One Hundred Years of Presbyterianism in Victoria" (1937).
Hamilton, R., "Jubilee History of the Presbyterian Church of Victoria" (1888).
(Image courtesy La Trobe Picture Collection, State Library of Victoria, A/S29/01/81/36)
Previous Article: Charles Stone (1819-98)
Next Article: Grace Alevina Sublet (c1834-1921)
Copyright © 2023 Travis M. Sellers. All rights reserved.

redpajama_set_name: RedPajamaCommonCrawl


text:
Florida Capitol's Festivus Pole Gets International Attention
WLRN 91.3 FM | By Gina Jordan
Chaz Stevens and his Festivus beer can pole meet with reporters in the Capitol.
Credit Margie Menzel/News Service of Florida
A 6-foot pole made ofPabstBlue Ribbon beer cans is making news around the world as it stands in Florida's Capitol building.
Maker Chaz Stevens and his beer-can pole have been featured on the Colbert Report, the Huffington Post, and the major networks.
"They were talking about me in Australia," Stevens told reporters in Tallahassee.
drove seven hours from his home in Deerfield Beach to display the pole celebrating Festivus, a parody holiday that
The show's characters decided that Dec. 23 should be a day "for the rest of us" who don't want to take part in the commercialism of Christmas.
Stevens, an atheist, made the trip after hearing about a nativity scene inside the Capitol.
"This is about separation of church and state," Stevens said. "The government should not be in the business of allowing religious symbols."
The pole will be on display until January 3.
"When I asked to put this up, I hoped that I could make a circus out of it. That was my intention," Stevens said. "The government doesn't belong here."
After hearing about the nativity, an array of groups sent requests to the Florida Department of Management Services to display their holiday messages, like the Tallahassee Atheists and the Satanic Temple of Tallahassee.
Pam Olsen with the said she's praying for Stevens as well as the group that posted a banner celebrating freedom from religion.
"It's Christ in Christmas, and that's why we put the nativity scene up," Olsen said. "I'm not sure what [the Festivus pole] has to do with Christmas or celebrating the season, but you know what? It's the freedom of speech to put it up here."
The competing displays led to a brief spat, with Stevens telling Olsen to remove the nativity.
"Well, it won't be removed, because we have freedom in America. Remember that, sir," Olsen said.
"We also have the separation of church and state government," Stevens replied.
Stevens said he expected a push back from Christians.
"What I didn't expect is the blow back from – ready for this -- Festivus purists who take great exception to a Festivus pole made out of beer cans," Stevens said. "They get really irritated."
Next stop for Stevens? He's pondering a Festivus beer-can pole in the nation's capital.
The News Service of Florida contributed to this story.
Copyright 2020 WLRN 91.3 FM. To see more, visit .
Gina Jordan
Gina Jordan reports from Tallahassee for WUSF and WLRN about how state policy affects your life.


text:
Rose Crest är en bergstopp i Antarktis. Den ligger i Östantarktis. Nya Zeeland gör anspråk på området. Toppen på Rose Crest är  meter över havet, eller  meter över den omgivande terrängen. Bredden vid basen är  km.

Terrängen runt Rose Crest är bergig åt nordväst, men åt sydost är den kuperad. Den högsta punkten i närheten är Apocalypse Peaks,  meter över havet,  kilometer väster om Rose Crest. Trakten är obefolkad. Det finns inga samhällen i närheten.

Kommentarer

Källor

Berg i Östantarktis
Nya Zeelands anspråk i Antarktis
Berg i Antarktis 2000 meter över havet eller högre

redpajama_set_name: RedPajamaWikipedia


Hotel Shanker is a historic heritage hotel, housed in a 19th-century palace in the heart of Kathmandu. It was the royal residence of the rulers of Nepal, from 1894 until 1964, when it was converted into a hotel. The facade and traditions were kept intact but the interiors were redesigned to give travelers the kind of comfort they'd expect of a world class hotel. The hotel is characterized by exquisite and authentic objects d'art. For example, the carved windows displayed in the lobby bar are over 200 years old.
How Indrajatra was celebrated in the 1930's - Duration: 3 minutes, 3 seconds.
Saturday BBQ at Hotel Shanker, Kathmandu, Nepal - Duration: 39 seconds.
Nepali Superstar Rajesh Hamal engagement at Hotel Shanker with Madhu Bhattarai - Duration: 13 minutes.
Spring Carnival! (Quick Recap!) Pashupati Paints, Hotel Shanker (Carnival Kathmandu Hotels) - Duration: 10 minutes.
ECS LIFE 1st Episode Kathmandu Hotels - Duration: 25 minutes.
Kathmandu Hotels Booking: "Secret Deal" at Hotel Shanker - Duration: 67 seconds.
A Garden Wedding Event at Hotel Shanker, Kathmandu - Duration: 53 seconds.
Video Guide to Book your stay Online -- Hotel Shanker (Kathmandu Hotels) - Duration: 4 minutes, 53 seconds.
Pokhara Information/Documentary -- Hotel Shanker Travel Desk - Duration: 22 minutes.
Meetings and Events at Hotel Shanker, Kathmandu http://www.shankerhotel.com.np - Duration: 99 seconds.
Mountain Flight (Mount Everest and the Greater Himalayas) - Duration: 5 minutes, 9 seconds.


What Have We Discovered In Extreme College That's Really Useful?
Youngsters who're in public colleges can take part in quite a lot of additional-curricular activities, akin to band, sports activities and golf gear. The kids additionally get plenty of socialization which will help of their later lives. They will encounter quite a lot of utterly totally different persona varieties.
I research the realm to discover a complete file of sources. Not one of many institutions pay or compensate for listings. discovered this text very helpful, My instructor stated it was correctly written and helpful. @sethughes, is an outstanding author and will make hi personal website online,(trace,hint 😉 ;Anyway, stage being, I discovered this webdite VERY helpful.
I like your enthusiasm, travelschooling! And you is perhaps right – all the pieces modifications for the entire household. For us the concept of finding out takes second place to dwelling life… and the educational happens naturally. Having stated that, there was a fraught half hour this morning whereas my daughter stamped her foot at doing her maths – it acquired carried out in the long term. It isn't all the time utterly blissful, sunny and smiley here!
High school is all in regards to the credit score you earn.
Congrats on being chosen for LOTD!! My kindergarten lecturers and my first grade instructor have been one of the best! Very sweet ladies who made school enjoyable and made me really feel cosy (I used to be an excessive introvert, and I moved from Nebraska to Louisiana proper earlier than kindergarten; subsequently, the alternative kids thought I talked humorous and made enjoyable of me!) I am so glad you went back to highschool and pursued your education and your dream to teach. Congratulations on making a difference within the lives of very younger children! Terrific lens.
People typically find themselves in jeopardy and confusion as soon as they attain a degree, after they stand at crossroads and are fully oblivious what to select from then onwards, and when circumstances and doubts come up and also you uncover indefinite solutions and options. You'll enormously revenue when a counselor takes management of the entire state of affairs with a related holistic technique. Thanks for penning this hub. My daughter mastered in particular education and works with kids of autism in an elementary college, so I am happy to share this with her. You provided a variety of useful and insightful advice.
Welcome to the official web site of Sweden.
One significantly annoying downside at my school is the quantity of school students miss for various actions, largely athletics. Right now alone, the softball workforce and volleyball staff have been every leaving college an hour early. Subsequent week is Homecoming, and the entire college day will probably be scale back short by an hour on Friday so the students can attend a Pep Rally.
So fascinating to find out about your childhood. It is nice to decelerate and bear in mind how life was once. The enjoyment of being grateful for what you had and not discontented over what you lack. I like your description of Christmas. Very sound suggestions and nice survival ideas and really correctly and articulately outlined.
Increased we adopt the European model of a stratified society, by which you rise by the combo of mental capability and arduous work. It's essential to eat to stay, and eating is less complicated (and cheaper) if you can make your particular person damn meals. One among my youngsters acquired what seems to be a prestigious tutorial award.


- Police in Charleston, South Carolina said they are searching for a missing 4-year-old girl after her mother was found brutally beaten Tuesday. Police setup a 24 hour tip line on Wednesday for citizens to report any information in the case of missing Heidi and a possible person of interest.
The four-year-old was wearing a hot pink top and blue trousers when she disappeared.
Police say she may be with a 25-30 year old, skinny, Hispanic male with short hair and dressed in all grey.
The Charleston Police Department said her mother was rushed to an area hospital after the school attended by two of her children call police reporting they did not show up and their mother did not call them in sick.
Police say the person of interest in her disappearance has facial tattoos, describing them as a lightning bolt and a flame. She was found around 4 p.m. EST on Wednesday in a business parking lot on Highway 78 near Depot Street in Riverside.
Riverside, Alabama, Police Chief Rick Oliver said 37-year-old Thomas Evans was arrested Wednesday after a police chase in Lauderdale County, Mississippi.
He also said Duterte's concern for women was evident in his repatriation of Filipino workers from Kuwait. According to a translation from the local media outlet Rappler, Duterte encouraged the act twice.
"There are many things we do not know.but one thing we know is Heidi Todd is missing", Tecklenburg added. He is with the mother at the hospital, authorities say.
"What could have been a day of great tragedy has really been a day of joy", Tecklenburg said.
The mother had four other children, two of whom were in the home at the time, according to Tecklenburg. "We don't know if Heidi might have been taken away in a vehicle or not".
A $10,000 reward is being offered by the Federal Bureau of Investigation for any information that leads to the girl's recovery.
Emergency crews searched for at least nine hours in the immediate area where Todd was reported missing Tuesday night, ending the immediate initial search effort around 3 a.m. Wednesday morning before resuming the search at daylight. The other children were unhurt, police say. Police and firefighters began searching for Todd around 2985 Sweetleaf Lane yesterday night.
But emergency officials said alerts sent out to residents about Todd's disappearance.
Users majorly reported that security standard of Windows 10 had been inspiring for their move to Windows 10. Microsoft also mentions that Defender ATP can run side by side with third-party antivirus solutions.
Police had previously been called to the home where 30-year-old Quentin Smith is alleged to have ambushed the two officers. Springfield Police Chief Lee Graf said the Springfield Police Division also will send representatives from the city.


text:
Asus/
Computex
The Asus Prime Utopia is a radical concept for the future of motherboards
By Sam Byford / @345triangle
May 29, 2019, 10:10 AM UTC |
Asus is celebrating its 30th anniversary this year, and as the company got its start as a motherboard maker back in 1989, it's fitting that it presents an idea of where it sees things going in the future. This concept is called Prime Utopia, and demonstrates what might be possible if we move away from the ATX standard that has dominated full-size desktop motherboard design since Intel introduced it in 1995.
Prime Utopia rearranges various components for greater efficiency. The PCIe slots are on the back, so the GPU can free up space while moving into a more stable position. There are four M.2 slots with a dedicated heatsink. Asus has also designed a proprietary "Hydra Cortex" fan header that lets individual fans be controlled independently.
Asus envisions I/O moving to Mini-PCIe modular components, so features like USB and Ethernet ports could be easily hot-swapped at will.
The motherboard also features a 7-inch OLED touchscreen that offers various readouts. Since this would only be useful for transparent or exposed builds, it comes in a Wi-Fi-equipped module of its own so that you can prop it on your desk to monitor system performance and control specific components like the fans.
Almost none of this would be possible with modern ATX motherboards, which have proven remarkably resilient over the past two and a half decades. Asus is far from the only company to suggest an alternative to ATX — even Intel itself has tried to move away from the standard. But breaking compatibility for case and component vendors would be a huge deal for the PC industry and surrounding ecosystem, so it's unlikely to happen any time soon.
Until it does, at least we have trade shows like Computex to pine over what could be.
Samsung Display shows off a new folding phone hinge that can rotate 360 degrees


Dear Reader. I have a confession. I did not visit every single one of the many hundreds of stands at IBC this year. In fact, I didnt even visit all 11 halls within the RAI. And I didnt talk to all 52,974 attendees. I was there. I have the stroopwafels to prove it. Its just that IBC is a massive show. And I am only one man. So, while this IBC round up is hopefully interesting and enlightening, it is far from comprehensive.
Right then, with that out of the way, here are the 10 innovations that either caught my eye - or I heard good things about - during my time in Amsterdam (13-17 September 2013).
The anticipated 4K camera from ARRI never materialized (well not in public anyway) but the current daddy of digital camera manufacturers did unveil something interesting. AMIRA is a documentary-style camera that combines the usual ARRI high image quality with an affordable (their words, not mine) CFast 2.0 workflow. The ergonomic design is optimized for single-operator use and extended shoulder-mounted operation. As the marketing bumpf will tell you, it is also ready to pick up and shoot straight out of the camera bag and features in-camera grading with preloaded looks based on 3D LUTs, as well as 200 fps slow motion.
To all intents and purposes this is a broadcast console for smaller OB trucks. Control is via a 17-inch multi-touch screen and a straightforward interface that accepts established finger gestures. Using Bluefin2 technology gives Callisto a pool of 180 channel processing paths, eight groups, four mains, 16 auxes, and 32 tracks. A Hydra2 router core provides Callisto with the same integral 8192 x 8192 as the larger Apollo and Artemis consoles.
Built using technology that was originally developed for flying devices, Freeflys MVI M10 is a handheld 3-axis digital stabilized camera gimbal that uses what they call active stabilization (unlike, say, Steadicam that uses passive stabilization). Capable of carrying up to 10lbs of camera (eg a Red Epic) its key feature is the Majestic Mode. This sees the gimbal take the operator's motion and convert it into stabilized pan and tilt movements, allowing for very low profile single operator setup and accurate framing in tight situations.
Looking for a cost-effective and painless way to incorporate UltraHD into a sport production environment? Check out this innovation from Joseph Fiber Solutions (JFS). A multifarious acquisition tool it is based around the Sony PMW-F55 4K camera with a Fujinon PL Series zoom lens plus JFS' own Studio Caddie-4K, a Dell computer and both AJA's Corvid Ultra high-frame-rate chassis and its Ki Pro Quad file-based recorder. The combination provides for 4K capture, replay, archiving, and live playout at what JFS insists will be half the cost of other systems.
Heres an idea that every competitor will want to poach. The Egg from TSL Products is a single-person QC unit for monitoring 5.1 surround sound and HD video. Providing an acoustically isolated environment for the operator, the ovoid sit-in device has a touch screen display that allows for video playback, router control, audio control, comms integration and video server control.
Using the same core as an ICON or a System 5 product, the Avid S6 console can control multiple Pro Tools and other EUCON-enabled DAWs (including Logic Pro and Nuendo) over an Ethernet connection. But most importantly, it is modular, ie, you can customize to your own requirements as you go along. Pre-configured S6 M10 or S6 M40 surfaces are available with the required faders, knobs, etc. already provided or, with S6 M40, further personalized with different channel control combinations.
The Science and Technology Council of the Academy of Motion Picture Arts and Sciences (AMPAS) is developing an iPad app. That is right. You read that correctly. Named the Academy Colour Predictor, and soon entering beta, it is being introduced to help filmmakers understand how key cinematography elements - lights, camera, filters, and subject matter interact with one another. Users can change any of the selected parameters to instantly visualise rendering differences and compare different combinations.
The Phantom Flex4K digital cinema camera can deliver 1000 frames per second high-speed video at - yes you guessed it - 4K resolution (4096x2160) and twice that in HD. The super 35mm sensor shooter outputs RAW images and includes hot-swappable Phantom CineMag IV storage plus 3G HD-SDI video outputs.
There were loads of excellent monitors on show at IBC but this one came highly recommended by a man who knows his stuff, so please go with it. The CM500TD is a 50-inch multi-format reference monitor for critical colour evaluation with 3G/dual-link/HD/SD-SDI, component, composite and DVI-I inputs. Featuring full 12-bit video processing and a 10-bit panel capable of reproducing over 1.073 billion colors on screen, it is also equipped with a passive circular polarizer and in-monitor multiplexing allowing for easy and affordable 3D monitoring (in addition to its 2D modes). Importantly, it offers support for virtually any signal format.
Colour grading and finishing for the budget-conscious is nothing new. But you dont necessarily expect if from Quantel, once the Rolls Royce of the FX and grading world. To hit the perceived market sweet spot, Pablo Rio 2KO sits on a cheaper PC platform than its older brother, the Pablo Rio, but has the same toolset and workflow. It is aimed squarely at broadcasters and post houses that work as far up as 2K and HD 3D but wont need to go near 4K. As with all Pablo Rio models, Pablo Rio 2KO is available as a fully blown system including storage, video I/O and the full Pablo Rio toolset, or as software only.


text:
Swalwell's graceful exit preserves bright future in politics
Swalwell's graceful exit preserves bright future in politics
Rep. Eric Swalwell, having just dropped out of the 2020 presidential race, laughed when I asked: Does he envision making another run at some point? He is, after all, just 38 years old. "You know, a lot of people would say, even as they were hosting me in their homes, 'If he's not president this time, he's going to to be president one day,'" Swalwell said in a phone interview. "And that's cold comfort because you're running really hard." He did not answer directly. Instead, he suggested he would be guided by the advice he gives to Capitol Hill interns, many of whom hold dreams of being elected to Congress. "First get involved in the issues you care about," he tells them, "and then you'll find the right office and the right way to serve." Swalwell had to know his bid was an extreme long shot from that sun-splashed April campaign kickoff rally at Dublin High School. Unlike Sen. Kamala Harris' grandiose opening in downtown Oakland, drawing 20,000 by organizers' account, Swalwell's few hundred supporters had to be urged to move closer to the stage to give the event a better look on TV. Vice President Joe Biden was not yet in the race and the Pete Buttigieg phenomenon was just starting to incubate, but Swalwell began well behind other contenders (Bernie Sanders, Elizabeth Warren, Cory Booker, Beto O'Rourke) in name recognition. As Swalwell noted at the time, only one U.S. House member — James Garfield, 1881 — has advanced straight to the presidency. He carried no illusions. Swalwell did not have a monopoly on the matter — every other Democrat was pushing for expanded regulation — but he took it further than any of the others in calling for a ban on assault weapons, along with a plan to buy back those already in circulation. He vowed to make gun control his campaign centerpiece. Prospective voters peppered him with concerns about every cause imaginable, most notably health care. But not a single American challenged him about his position on guns. No one demanded, "You're not taking my gun," he said. This for the congressman who gets trolled so regularly and viciously on social media that even his Facebook post about his son Nathan's first birthday elicited a flurry of hate from gun advocates. "Front and center, eyeball to eyeball, is not the same as online," Swalwell said, adding at another point, "What I learned was that (gun control) is not the hot stove that we've always been told." The congressman said he found it gratifying that other candidates — notably Sanders and Harris — have stiffened their gun control positions as the nomination fight advances. As the first major candidate to drop out, Swalwell has been praised not only for his acceptance of reality — if only others in the bottom tier should take note, pleaded columnist Jennifer Rubin in the Washington Post — but for the classy way he did it. Unlike so many politicians in defeat, he issued neither excuses nor shots at the remaining contenders, on or off the record. At his farewell news conference, he thanked the news media he encountered along the way. "They ask the tough questions we expect in a democracy," he said. In retrospect, the three-month campaign was a no-lose venture for a young congressman on a leadership track. His role in the Russian investigations will surely keep him on the cable news circuit, and his campaign's emphasis on gun control will make him a go-to source on that perennial issue. As Swalwell departs the race, another candidate from the San Francisco Bay Area jumped in. Tom Steyer, a former hedge fund investor who became a leading benefactor of liberal candidates and causes, will try to position himself as a populist outsider. Steyer has never held elective office, but he will be taken seriously from the start due to the $100 million he plans to pour into his campaign. His personal fortune is likely to be a blessing and a curse in a Democratic primary where the words "Wall Street" and "billionaire" are popular pejoratives. It will buy him an abundance of advertising and staff, but it also will raise questions about how he earned it. The Los Angeles Times was fast on the heels of his announcement with a story describing his hedge fund's history: from his letter advising clients how to use offshore investments to avoid U.S. taxes to his fund's investments in coal and private prisons. Steyer has been a champion of climate change action and the impeachment of President Trump — but that hardly distinguishes him in a field where those positions are de rigueur. San Francisco has long been a place that fuels presidential races with money, not candidates. There has never been a year quite like this, with the city's former district attorney, Sen. Kamala Harris, rising in the top tier and two others with local pedigree, Swalwell and now Steyer, taking a shot at the big prize. "I'm the first one out, so I wouldn't say our campaign is the model for any others," he said with a laugh. "But one thing I stuck to rigidly was to not follow the herd mentality … be confident in yourself." It's not easy in today's 24-hour news cycle to avoid being drawn into the latest poll, opponent's statement or incremental development in the news. "You go up and down, up and down, almost every hour," Swalwell said. "The biggest challenge is how do you stay constant." Before joining the opinion pages, he directed the newspaper's East Bay news coverage. He started at The Chronicle in 1990 as an assistant city editor. John began his journalism career as a reporter for the Red Bluff Daily News. Two years later, he was promoted to the Washington, D.C., bureau of the newspaper's parent company, Donrey Media Group. After that, he worked as a general assignment reporter for the Associated Press in Philadelphia and as a statehouse reporter and assistant city editor for the Denver Post. He graduated from Humboldt State University in 1977 with a degree in journalism. He received a Distinguished Alumni Award from HSU in 2009 and was the university's commencement speaker in 2010.
Remainer Revenge: Chancellor Hammond threatens Commons 'occupation' block no deal Brexit
The idea originally mooted by former Brexit Secretary Dominic Raab before his elimination from…
Met police launch investigation into leaked Darroch cables
Police have opened an investigation into the alleged leaking of diplomatic cables involving the outgoing UK ambassador to Washington, Sir Kim …
Posted on Author adminoneCategories Politics
Previous Previous post: Diverse City: The Ethnic Show
Next Next post: Diplomatic remarks


text:
Good Enough To Keep!
Charlie Christian (1916 – 1942) was an American swing and bebop jazz guitarist. He was an important early performer on the electric guitar, and is cited as a key figure in the development of bebop, cool and modern jazz. Many critics believe that he alone is the link between hot and modern jazz; there is jazz before Charlie Christian and jazz after Charlie Christian.
Charlie Christian grew up in Oklahoma City, his father was a blind guitarist and singer, his two elder brothers, Edward and Clarence, were musicians, and Charlie himself started early on playing cigar-box "guitar" during his elementary school days. When he grew up, he became a much-admired local musician in Oklahoma, playing an amplified acoustic guitar as early as 1937. Word of his skill reached John Hammond, who arranged for Christian to travel to Los Angeles in August 1939 for an audition with Benny Goodman. Goodman was deeply impressed by Christian's playing, engaged him and soon featured him on weekly radio broadcasts and in recordings. Before the year was over he was a nationally prominent jazz soloist, unfortunately his success was as brief as it was immediate. Charlie contracted tuberculosis in mid-1941 and died a few months later.
Christian was among the first jazz guitarists to amplify his instrument in order to match the volume of wind instruments, and he was clearly the most brilliant soloist of his time on electric guitar. He was emulated by many swing-style players, and his posthumous impact on younger bop guitarists was enormous. He was a regular participant in the Harlem jam sesseions at Minton's at which some of the bop pioneers gathered - in this setting Charlie further developed his playing style and became the first bop guitarist.
Charlie Christian remains among the most creative soloist of the swing period, and his co-operate work with Goodman created compositions and memorable recordings that since have become standards in jazz. I found a couple of examples of Goodman-Christian compositions on YouTube I would like to share.
The first video is a recording of a performance by Benny Goodman septet at the North Sea Festival, 1982. Bandmembers are Benny Goodman (Clarinet), Scott Hamilton (Tenor), Warren Vache (Cornet), Chris Flory (Guitar), Phil Flanagan (Bass), John Bunch (Piano), Mel Lewis (Drums). The tune played is "Air Mail Special" - also known as "Good Enough To Keep"
The secound video fragment is by an unnamed ensemble playing "Breakfast Feud" performed ive at FNAC Callao Madrid November 9th 2006
Labels: charlie christian
posted by Jo at 12:23 AM
Thanks Jo for this great starter.
Charlie Christian is one of the most important guitar players in music as he was one of the key figures in jazz.
BTW: Thanks for this subject: I was affraid I had to read something about: ain't gonne rain no more / i get the blues when it rains / into each life some rain must fall / rainbow of my dreams
just like a rainbow / keeps on a rainin' / don't mind the rain
rainy nights / it ain't gonna rain no more / left my sugar standing in the rain / rain / it don't do nothin' but rain / garden in the rain / rainy days / singing in the rain / new fallin' rain blues / my bluebird was caught in the rain / i don't mind walkin' in the rain /
smile when the raindrops fall / rainy days / rain on the roof
Thanks for that !!
The Five Guitars - a tribute to Charlie Byrd
Rita Reys
Peter Herbolzheimer
Musical Mountaineers
Luis Salinas
Gardenias For Lady Day
Song For Linda, Nelly, Frank and Hans
Grant Green


text:
Secrets of the Night / Charles Marion Russell
Download Add Order Contact
From Nancy C. Russell to Charles M. Russell
Thousand Stand in Streets during Funeral Services
Coyote Chasing Steer
Art Item Information
©Gilcrease Museum
Title(s):
Secrets of the Night
Charles Marion Russell;
Roman Bronze Works;
Dr. Philip G. Cole Collection
modeled 1926; lost-wax cast circa 1926
Materials/Techniques:
lost-wax cast in bronze
Overall: 13 x 5 7/8 in. (33 x 14.9 cm)
Bronze Sculpture
Gift of the Thomas Gilcrease Foundation, 1955
Marks/Inscriptions: Signed with colophon, "C.M. Russell" [Trademark buffalo skull]; Marked, "Roman Bronze Works N-Y-".
Curatorial Remarks:
The spear was cast separately and added to the sculpture. The bottom of the bronze is closed off with sheet metal. It was purchased by Philip G. Cole in March 1927.
Information given by Ann Boulton Young, Associate Conservator for the Gilcrease Museum, 2018
From Gilcrease Museum:
Role(s):
From Getty's Union List of Artist Names:
Names (all):
Russell, Charles Marion
Death Date:
Nationalities:
American (North American)
American painter, sculptor, and illustrator, 1864-1926
active (professional function)
Comment on works: painter; sculptor
Related People:
Scheuerle, Joe, friend of - person
American painter, illustrator, and etcher, 1873-1948
Seltzer, Olaf Carl, friend of - person
American painter and illustrator, 1877-1957
Roman Bronze Works
Tags and Search Terms
Animal, Art, bird (animal), bronzes, Charles M. Russell artwork, crouching, Kneeling, long hair, man, Native American, night, owl (bird), rock, sculpture, spear, wind, wings
Art by Charles M. Russell
Charles M. Russell Artworks in Gilcrease Collection
Renowned as an iconic figure in 20th century American art for his portrayals of the American West, Gilcrease Museum houses and displays masterworks from the prolific life of artist Charles M. Russell. Significant samplings of Charles M. Russell's mature painting style is enriched by Gilcrease Museum's equally important collection of the artist's bronze sculptures, sketches, and personal belongings. In addition to the Charles M. Russell paintings and sculptures in the museum's permanent art collections, the museum archives is the proud home of the Charles M. Russell Research Collection (Britzman). The research collection's catalog of preparatory drawings, sketches, and illustrated letters adds to the depth and understanding of Charles M Russell's life and artistic process.
Russell, Charles. Secrets of the Night. 0837.18. modeled 1926; lost-wax cast circa 1926. Tulsa: Gilcrease Museum, https://collections.gilcrease.org/object/083718 (03/26/2019).
Our Online Collections site is a work in progress. If you have information about this item that may be of assistance, please contact us.


text:
<!doctype html>

    <title>Registration information - PyGotham 2016</title>
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1.0">
    <link rel="stylesheet" href="../../static/css/app.css">

    <meta name="msapplication-TileColor" content="#182833">
    <meta name="msapplication-TileImage" content="/static/img/metro-icon.png">
    <link rel="apple-touch-icon-precomposed" href="../../static/img/apple-touch-icon.png">
    <link rel="icon" href="../../static/img/favicon.png">

          Menu

              About

Code of Conduct

FAQ

Privacy Policy

What is PyGotham?

              Events

Social

Talk List

Talk Schedule

              Registration

Information

              Speaking

Call for Proposals

              Sponsors

Sponsors

Sponsorship Prospectus

              Venue

Hotels

Information

Registration

Registration for PyGotham 2016 is no longer open.

Tickets

The following ticket options are available. Select the one that is most
      appropriate for your type of registration.

            Registration
            Early Bird Rate
            Regular Rate

            Corporate

            $200

            Individual
            $50
            $100

            Student

            $50

Scholarships

We aim for PyGotham to be open to all to attend, and we strive to make
        the conference as accessible as possible. If you aren't able to obtain a
        ticket for financial or other reasons, please fill out the application
        at
        https://goo.gl/forms/uEQ55S18V5, and we'll arrange for a reduced
        amount or a free scholarship ticket to ensure that you can attend. Feel
        free to ping us at
        scholarships@pygotham.org if you have any questions.

What's Included?

Along with your conference registration, attendees will receive
      breakfast, lunch, and break refreshments.

Refund Policy

Refunds requested more than 48 hours prior to the start of the event
        will be processed, resulting in a return of the full purchase price of
        the ticket. (Corporate sponsors who include an additional donation,
        please specify if you wish to have the donation returned as well.)

 We apologize that within 48 hours of the event, catering and capacity
        numbers will be locked in. We will not be able to provide a refund at
        that time.

        PyGotham 2016 is a production of Big Apple Py.

        Artwork by Jessie Sima. UX by Allison Cameron. Hosting provided by Rackspace.

        Questions? Comments? Please contact organizers@pygotham.org.

redpajama_set_name: RedPajamaGithub


text:
Batman: Arkham Origins Blackgate – Deluxe Edition for Playstation 3 , Xbox 360, Wii U and PC
Posted On April 1, 2014 April 3, 2016 By James Jarvis
Warner Bros. Interactive Entertainment and DC Entertainment today are releasing Batman™: Arkham Origins Blackgate – Deluxe Edition for digital download on the PlayStation®3 computer entertainment system, Xbox 360 games and entertainment system from Microsoft, Wii U™ system and PC.
Enhanced HD graphics, new content for ultimate Blackgate experience Available now as instant digital download only
Developed by Armature Studio, Batman: Arkham Origins Blackgate – Deluxe Edition enhances the core pillars of the previously released handheld version of the game with high-definition visuals, an all-new map system, new enemy encounters, difficulty levels, and batsuits. Fans can begin downloading the game today on the PlayStation®Network, Xbox Live Games Store, Nintendo eShop and STEAM. The game is scheduled for release in Europe and other international territories beginning 1st of April on PC and in the Xbox Live Games Store, 2nd of April on the PS3™, and later in April on the Wii U.
Previously only available for PlayStation®Vita handheld entertainment system and Nintendo 3DS™ handheld system, and created as a companion game to Batman: Arkham Origins, Batman: Arkham Origins Blackgate – Deluxe Edition features enhanced high-definition 2.5-D graphics and, 5.1 surround sound. Players will be able to guide their way through Blackgate prison with the new navigational system created for this version of the game. In addition, they can suit up with the exclusive Zero Year Batsuit skin which players can unlock by registering for a Warner Bros. ID (WBID) account.
Set three months after Batman: Arkham Origins, Batman is summoned to restore peace and order within the walls of Blackgate Prison. Players will explore the depths of the island penitentiary as Batman investigates and realizes that there is more to the henchman uprising than initially meets the eye.
Batman: Arkham Origins Blackgate – Deluxe Edition is based on DC Comics' core Batman license and rated PEGI 16. Fans can visit www.batmanarkhamorigins.com for more information about the game.
Batman Arkham: Origins Blackgate DE Out Today For Xbox 360, Tomorrow for PS3
'Batman: Arkham Origins Blackgate – Deluxe Edition' Available Now
Batman: Arkham Origins Blackgate – Deluxe Edition out today, new trailer celebrates launch
Batman: Arkham Origins Blackgate delayed on Wii U
Batman: Arkham Origins Blackgate launches on Xbox 360
Batman: Arkham Origins Blackgate Deluxe Edition Confirmed for April Release
Batman: Arkham Origins Blackgate Deluxe Edition listed on Xbox 360
'Batman: Arkham Origins Blackgate – Deluxe Edition' (ALL) Announced – Screens & Trailer
Batman: Arkham Origins Blackgate – Deluxe Edition heading to consoles
#Gaming #News
Tagged: Arkham Origins Blackgate Deluxe Edition batman Batman Arkham Origins Blackgate Deluxe Edition cinema concerts Entertainment expos Gadgets games gaming its much more itsmuchmore itsmuchmore.com local news movies music nintendo Nintendo eShop nottingham pc PlayStation 3 PlayStation Network theatre tv Video Games Warner Bros. Warner Bros. Interactive Entertainment wii u Xbox 360
The Vamps announce Forest Live summer dates
Posted On : February 18, 2015
Classic Thriller Season – 25 years of thrilling entertainment for Nottingham
Posted On : July 13, 2013
Table Top Racing: World Tour – Nitro Edition Speeds onto Switch with Split Screen Multiplayer 1st May 2019!
Posted On : April 22, 2019
Previous post: King of the Jungle returns to the Forest!
Next post: Summer Season announced for the Theatre Royal and Royal Concert Hall Nottingham


text:
MLB Analysis & Sabermetrics
Tigers' Nick Castellanos is struggling to adjust to MLB pitching
After showing flashes of promise in 2014, MLB pitchers have adjusted to Nick Castellanos. He has not adjusted back.
By Rob Rogacki@BYBRob May 27, 2015, 11:00am EDT
Share All sharing options for: Tigers' Nick Castellanos is struggling to adjust to MLB pitching
Tim Fuller-USA TODAY Sports
Throughout Nick Castellanos' rise through the Detroit Tigers farm system, fans were told about his immense offensive potential. While opinions varied slightly on just how high his ceiling was, many viewed Castellanos as a future .280-.300 hitter with 20-25 home run potential. He was (and still is) supposed to be a middle-of-the-order bat that will supplement Miguel Cabrera and company as the Tigers move into the latter half of the decade.
That rise to stardom hasn't happened yet. Castellanos is hitting .255/.301/.391 with 15 home runs in 773 career plate appearances in a Tigers uniform. However, he is still only 23 years old and less than two months into his second full season in the major leagues. There is plenty of time for him to find his groove and become the hitter that scouts thought he could become.
Many predicted that 2015 would be a breakout season for Castellanos. He showed flashes of potential last season, hitting .259/.306/.394 with 11 home runs and 66 RBI in 579 plate appearances. That predicted breakout has instead turned into a sophomore slump, and Castellanos is batting just .241/.290/.395 this year.
Last season, Castellanos displayed some interesting platoon splits. He hit for a higher average against right-handed pitchers, but walked more against lefties. His isolated power (ISO) was nearly identical against both righties and lefties. This season, those splits are a different story. Castellanos is hitting .320/.414/.460 in 29 plate appearances against left-handed pitchers, and .226/.265/.401 in 147 plate appearances against righties.
The drop-off in performance against righthanders is startling, but there is a reason for his decline. Last season, Castellanos hit .309 with a .462 slugging average against fastballs thrown by right-handed pitchers. He also did plenty of damage on pitches thrown on the inner half. This season, righthanders have adjusted. They are throwing more offspeed pitches, and pitching Castellanos away more often than in 2014.
Castellanos has not helped matters. He is swinging at 38.8 percent of pitches thrown outside of the strike zone, a big increase from the 33.6 percent he swung at in 2014. His overall contact rate, one of the worst in baseball at 72.8 percent last season, has not improved much. He is making contact with a higher percentage of pitches outside the strike zone, resulting in a drop in his line drive rate and batting average on balls in play (BABIP). His swinging strike rate has risen to 14.2 percent, and he is having a lot of trouble laying off pitches down and away.
How does he fix this? Castellanos has shown flashes of his lofty potential during his MLB career, and has done very well when swinging at pitches on the inner half of the plate. However, until he can improve his pitch recognition skills and lay off the pitches he is swinging over on the outer half, pitchers have no incentive to work into his wheelhouse on the inner third. Castellanos could also look to punch the ball to the opposite field more often, something he has gotten away from in 2015.
While this trend is a bit concerning, I don't think it is time to worry about Castellanos yet. He is still only 23 years old and has fewer than 800 career plate appearances at the MLB level. He is still filling out his large, 6'4" frame, and has basically had to learn a new defensive position over the past year. As long as he can make the necessary adjustments and start laying off more pitches, we should start to see more of the Castellanos that everyone expected during his rise through the farm system.


text:
Q: Signal R hub start hang up I have a .net console application that call a signal R hub method.
I managed to configure the connection to restart after several failure and start a fresh hub instance after the retry count exceeded.
The problem is sometimes hub.start method will hang up without any exception and it did not enter the continuation.
Here is the code:
 private static void restart()
    {
        Logging("Restarting connection", EventLogEntryType.Warning);

        hubConnection.Start() // it stuck without any error after several retry
            .ContinueWith((t) =>
        {

            if (restartCount <= restartRetryCountMax)
            {
                if (t.IsFaulted)
                {
                    restartCount++;
                    restart();
                }
                else
                {
                    CheckClientStatus();
                }
            }
            else
            {
                restartCount = 0;
                Logging("Initialize new connection", EventLogEntryType.Information);
                start();//start a fresh hub instance
            }
        });
    }

Is this a bugs ?
I'm using signalr version 2.2.0

redpajama_set_name: RedPajamaStackExchange


My sister began to show me faces that you would ordinarily miss unless you looked very closely in the background of pictures, on clothing, on the wall of a building, on peoples clothing, curtains, and just tossed laundry hanging on a chair. These faces don't look friendly. Do you know what they are and why they are here? Can everyone see them, or just some people? Do you think purging will remove them? Or could they be the eyes of the LORD that are in every place beholding the evil and the good? I am very spiritual.
I have been awakened in my home by what sounded like angels wings moving quickly down the hall. I got up and looked to see if my hubby was home early from work to see no one. Well we are just renters at our present home. I did once live in a home where I felt the presence of someone sitting on the bed beside me, and turned over to see no one.
A few strange things occurred in that place, and early as an adult, I had that awful sleep paralysis happen a few times. It was scary. I felt like I was being held down, and the more I struggled to get free the harder it got. When I relaxed it left me. Felt like a force that started at my feet and moved up all the way over my body, and once it got all the way over I got free.
My family is very sensitive to the spiritual world. I had an uncle who died from cancer. When he was sick, he said he saw the devil in his home and was frightened to go to sleep a few nights afterwards. I know this is a lot, just giving you some family history. Anyway thanks for your time and look forward to hearing from you. My hubby thinks we are all nuts, the whole family, yet he too admitted he saw the faces, once my sister showed him.
I have to tell you, I definitely love imagination. I hear from my peeps that imagination is a vital key to moving on to doing great things. Imagination is a world where there are no boundaries and creativity work hand in hand. Its where normal meets abnormal and we put square blocks in round holes. With imagination, everything works in unison. Know that thoughts are real things and suggestion is a powerful word. Being influenced by others through suggestion happens all the time and us empaths get caught up in what the source is trying to send out. In this case it is faces of all kinds. I understand from my peeps there is an insecurity issue of being watched coming from someone. I am not clear on who it is, but it is in the air. Imagination stirs the thought process into creating and there the faces are. Tell yourself all is good and find other more comfortable images that can also be created. Do not get caught up in this good and bad stuff as it will send you spiraling into a rabbit hole.
I hear you do not have to purge anything, but if you want to feel more comfortable you can smudge your home or have some prayers of cleansing and love spoken throughout the home. This can also be done at the workplace as I am not sure where you first picked up this energy.
Being awakened at home of noises is also common everywhere. I hear from my peeps that indeed angels are around your home as they are being asked to help in matters of urgency. Know that the angels are there and bringing in love to your home. Put thought into being surrounded by the divine white light at all times, even during sleep as this will help in keeping negative energy from getting close to you. This will also help in better sleep time. If you feel there is a negative energy present, you need to stand up to the spirit and tell it to cross over because it is now time to move on. You must be in control at all times. You mention the paralysis and this is just you leaving your body at night and you are having a hard time getting back into your body. You have a soul, spirit and identical energy fields of yourself that connect with the universe at night and travel.
Work with your angels always. Ask Arch Angel Michael to remove any negative attachments that you may have. This will help in how you are feeling during the day and ask anytime you feel down.
I do not feel any horrible energy around you so I hope this puts your mind at ease. At night say a prayer or mantra before bed of what you would like to be feeling and getting for tomorrow. Also add in surrounding yourself in the Divine White Light of Love during sleep as this will help in a more calming sleep. The power of suggestion is POWERFUL. I hope this helps.


Search for chamber music repertoire by limiting works by composer or instrumentation.
After setting search criteria above, click the "Search Repertoire" button. A list of the repertoire will appear in a new page. Click the "details" link next to any repertoire to view full details.